Merge branch 'v8.6'

2 files changed, 35 insertions, 36 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index db8cbf2313..a063cbbfe3 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")
@@ -2094,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")
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index c13e8fc28f..b4c6d032bf 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -294,18 +294,6 @@ struct
   else  XO (index (n lsr 1))
 
 
- let idx n =
-  (*a.k.a path_of_int *)
-  (* returns the list of digits of n in reverse order with initial 1 removed *)
-  let rec digits_of_int n =
-   if Int.equal n 1 then []
-   else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1))
-  in
-   List.fold_right
-    (fun b c -> (if b then XI c else XO c))
-    (List.rev (digits_of_int n))
-    (XH)
-
  let z x =
   match compare x 0 with
    | 0 -> Z0