Fix Bug #5073 : regression of micromega plugin

esprit d'escalier : is now also fixed for R

1 files changed, 20 insertions, 15 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 23d37c273..a063cbbfe 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -2100,22 +2100,27 @@ let micromega_genr prover tac =
        let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; 
                                                     micromega_order_changer res' env' ff_arith ] in
 
+       let goal_props = List.rev (prop_env_of_formula ff') in 
+
+       let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in 
+       
+       let arith_args = goal_props @ goal_vars in
+
        let kill_arith = 
-         Tacticals.New.tclTHEN
-           (Tactics.keep [])
-           ((*Tactics.tclABSTRACT  None*)
-             (Tacticals.New.tclTHEN tac_arith tac)) in 
-
-
-       Tacticals.New.tclTHEN
-         (Tactics.forward true (Some (Some kill_arith)) (ipat_of_name goal_name) arith_goal)
-        
-         (Tacticals.New.tclTHENLIST
-               [(Tactics.generalize (List.map Term.mkVar ids));
-                Tactics.unfold_constr coq_not_gl_ref;
-                (Tactics.apply (Term.applist (Term.mkVar goal_name,List.rev (prop_env_of_formula ff'))))
-               ]
-         )
+           Tacticals.New.tclTHEN
+             (Tactics.keep [])
+             ((*Tactics.tclABSTRACT  None*)
+                (Tacticals.New.tclTHEN tac_arith tac)) in 
+
+       Tacticals.New.tclTHENS
+         (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal)
+         [
+           kill_arith;
+           (Tacticals.New.tclTHENLIST
+            [(Tactics.generalize (List.map Term.mkVar ids));
+             Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args))
+            ] )
+         ]
 
     with
     | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")