Fix Bug #5073 : regression of micromega plugin

The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm)
instead of apply (__arith P1 ... Pn) which unification could fail.

1 files changed, 15 insertions, 9 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index db8cbf231..23d37c273 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -961,7 +961,7 @@ struct
           let (env,n) = _add l ( n+1) v in
            (e::env,n) in
     let (env, n) =  _add env 1 v in
-     (env, CamlToCoq.idx n)
+     (env, CamlToCoq.positive n)
 
    let get_rank env v = 
 
@@ -1986,21 +1986,27 @@ let micromega_gen
                                                     micromega_order_change spec res'
                                                       (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) 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
+       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.unfold_constr coq_not_gl_ref;
-                (Tactics.apply (Term.applist (Term.mkVar goal_name,List.rev (prop_env_of_formula ff'))))
-            ])
-                (*Tacticals.New.tclTRY(Tactics.apply_with_bindings_gen true false
-                  [None,(Loc.ghost,((Term.mkVar goal_name) ,Misctypes.NoBindings))]*)
+             Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args))
+            ] )
+         ]
     with
     | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
     | Mfourier.TimeOut  -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")