Merge v8.5 into trunk

Conflicts:
	tactics/eauto.ml4

(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)

1 files changed, 63 insertions, 22 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index f2860a2300..ea74dc37ea 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -165,10 +165,10 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-  let ct = pf_type_of gl c in
-  let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
-  let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in
-   [eqclause]
+  let sigma, ct = pf_type_of gl c in
+  let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
+  let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
+  [eqclause]
 
 let rewrite_conv_closed_core_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
@@ -944,7 +944,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
 
 let onEquality with_evars tac (c,lbindc) =
   Proofview.Goal.nf_enter begin fun gl ->
-  let type_of = pf_type_of gl in
+  let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
   let t = type_of c in
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
@@ -1019,7 +1019,7 @@ let find_sigma_data env s = build_sigma_type ()
 let make_tuple env sigma (rterm,rty) lind =
   assert (dependent (mkRel lind) rty);
   let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
-  let sigma, a = e_type_of ~refresh:true env sigma (mkRel lind) in
+  let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
   let (na,_,_) = lookup_rel lind env in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
   let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1053,7 +1053,7 @@ let minimal_free_rels_rec env sigma =
   let rec minimalrec_free_rels_rec prev_rels (c,cty) =
     let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
     let combined_rels = Int.Set.union prev_rels direct_rels in
-    let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i)))
+    let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i)))
     in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
   in minimalrec_free_rels_rec Int.Set.empty
 
@@ -1099,7 +1099,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let rec sigrec_clausal_form siglen p_i =
     if Int.equal siglen 0 then
       (* is the default value typable with the expected type *)
-      let dflt_typ = type_of env sigma dflt in
+      let dflt_typ = unsafe_type_of env sigma dflt in
       try
 	let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
 	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
@@ -1118,7 +1118,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
           (destEvar ev)
       with
 	| Some w ->
-            let w_type = type_of env sigma w in
+            let w_type = unsafe_type_of env sigma w in
             if Evarconv.e_cumul env evdref w_type a then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
@@ -1200,7 +1200,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
     sigma, (tuple,tuplety,dfltval)
 
 let rec build_injrec env sigma dflt c = function
-  | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c)
+  | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c)
   | ((sp,cnum),argnum)::l ->
     try
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1253,7 +1253,7 @@ let inject_if_homogenous_dependent_pair ty =
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
-    let new_eq_args = [|pf_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
+    let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
@@ -1293,7 +1293,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let injfun = mkNamedLambda e t injbody in
       let sigma,congr = Evd.fresh_global env sigma eq.congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
-      let sigma, pf_typ = Typing.e_type_of env sigma pf in
+      let sigma, pf_typ = Typing.type_of env sigma pf in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
       let pf = Clenvtac.clenv_value_cast_meta inj_clause in
       let ty = simplify_args env sigma (clenv_type inj_clause) in
@@ -1460,8 +1460,8 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
   let expected_goal = nf_betaiota sigma expected_goal in
   (* Retype to get universes right *)
-  let sigma, expected_goal_ty = Typing.e_type_of env sigma expected_goal in
-  let sigma, _ = Typing.e_type_of env sigma body in
+  let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
+  let sigma, _ = Typing.type_of env sigma body in
     sigma,body,expected_goal
 
 (* Like "replace" but decompose dependent equalities                      *)
@@ -1662,26 +1662,40 @@ let default_subst_tactic_flags () =
   else
     { only_leibniz = true; rewrite_dependent_proof = false }
 
+let regular_subst_tactic = ref false
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "more regular behavior of tactic subst";
+      optkey   = ["Regular";"Subst";"Tactic"];
+      optread  = (fun () -> !regular_subst_tactic);
+      optwrite = (:=) regular_subst_tactic }
+
 let subst_all ?(flags=default_subst_tactic_flags ()) () =
 
+  if !regular_subst_tactic then
+
   (* First step: find hypotheses to treat in linear time *)
   let find_equations gl =
     let gl = Proofview.Goal.assume gl in
+    let env = Proofview.Goal.env gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let test (hyp,_,c) =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose c in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
-        (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-        if Term.eq_constr x y then None else
         match kind_of_term x, kind_of_term y with
-        | Var _, _ | _, Var _ -> Some hyp
-        | _ -> None
+        | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z))  ->
+            Some hyp
+        | _ ->
+            None
       with Constr_matching.PatternMatchingFailure -> None
     in
     let hyps = Proofview.Goal.hyps gl in
-    List.map_filter test hyps
+    List.rev (List.map_filter test hyps)
   in
 
   (* Second step: treat equations *)
@@ -1694,9 +1708,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
     if Term.eq_constr x y then Proofview.tclUNIT () else
       match kind_of_term x, kind_of_term y with
-      | Var x, _ -> subst_one flags.rewrite_dependent_proof x (hyp,y,true)
-      | _, Var y -> subst_one flags.rewrite_dependent_proof y (hyp,x,false)
-      | _ -> Proofview.tclUNIT ()
+      | Var x', _ when not (occur_term x y) ->
+          subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
+      | _, Var y' when not (occur_term y x) ->
+          subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
+      | _ ->
+          Proofview.tclUNIT ()
     end
   in
   Proofview.Goal.nf_enter begin fun gl ->
@@ -1704,6 +1721,30 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     tclMAP process ids
   end
 
+  else
+
+(* Old implementation, not able to manage configurations like a=b, a=t,
+   or situations like "a = S b, b = S a", or also accidentally unfolding
+   let-ins *)
+  Proofview.Goal.nf_enter begin fun gl ->
+  let find_eq_data_decompose = find_eq_data_decompose gl in
+  let test (_,c) =
+    try
+      let lbeq,u,(_,x,y) = find_eq_data_decompose c in
+      let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+      if flags.only_leibniz then restrict_to_eq_and_identity eq;
+      (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
+      if Term.eq_constr x y then failwith "caught";
+      match kind_of_term x with Var x -> x | _ ->
+      match kind_of_term y with Var y -> y | _ -> failwith "caught"
+    with Constr_matching.PatternMatchingFailure -> failwith "caught" in
+  let test p = try Some (test p) with Failure _ -> None in
+  let hyps = pf_hyps_types gl in
+  let ids = List.map_filter test hyps in
+  let ids = List.uniquize ids in
+  subst_gen flags.rewrite_dependent_proof ids
+  end
+
 (* Rewrite the first assumption for which a condition holds
    and gives the direction of the rewrite *)