Merge branch 'v8.5'

2 files changed, 52 insertions, 40 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index bc03baf26..cb1d82ae6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1610,6 +1610,17 @@ user = raise user error specific to rewrite
 (**********************************************************************)
 (* Substitutions tactics (JCF) *)
 
+let regular_subst_tactic = ref true
+
+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 restrict_to_eq_and_identity eq = (* compatibility *)
   if not (is_global glob_eq eq) &&
     not (is_global glob_identity eq) 
@@ -1638,24 +1649,25 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   (* The set of hypotheses using x *)
   let dephyps =
-    List.rev (snd (List.fold_right (fun dcl (deps,allhyps) ->
+    List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) ->
       let id = get_id dcl in
       if not (Id.equal id hyp)
          && List.exists (fun y -> occur_var_in_decl env y dcl) deps
       then
-        ((if is_local_assum dcl then deps else id::deps), id::allhyps)
+        let id_dest = if !regular_subst_tactic then dest else MoveLast in
+        (dest,(if is_local_assum dcl then deps else id::deps), (id_dest,id)::allhyps)
       else
-        (deps,allhyps))
+        (MoveBefore id,deps,allhyps))
       hyps
-      ([x],[]))) in
+      (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *)
   (* Decides if x appears in conclusion *)
   let depconcl = occur_var env x concl in
   let need_rewrite = not (List.is_empty dephyps) || depconcl in
   tclTHENLIST
     ((if need_rewrite then
-      [revert dephyps;
+      [revert (List.map snd dephyps);
        general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp);
-       (tclMAP intro_using dephyps)]
+       (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)]
       else
        [Proofview.tclUNIT ()]) @
      [tclTRY (clear [x; hyp])])
@@ -1706,17 +1718,6 @@ let default_subst_tactic_flags () =
   else
     { only_leibniz = true; rewrite_dependent_proof = false }
 
-let regular_subst_tactic = ref true
-
-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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a626092dd..0bb842601 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1836,19 +1836,19 @@ let on_the_bodies = function
 | [id] -> str " depends on the body of " ++ pr_id id
 | l -> str " depends on the bodies of " ++ pr_sequence pr_id l
 
-let check_is_type env ty msg =
-  Proofview.tclEVARMAP >>= fun sigma ->
+exception DependsOnBody of Id.t option
+
+let check_is_type env sigma ty =
   let evdref = ref sigma in
   try
     let _ = Typing.e_sort_of env evdref ty in
-    Proofview.Unsafe.tclEVARS !evdref
+    !evdref
   with e when Errors.noncritical e ->
-    msg e
+    raise (DependsOnBody None)
 
-let check_decl env decl msg =
+let check_decl env sigma decl =
   let open Context.Named.Declaration in
   let ty = get_type decl in
-  Proofview.tclEVARMAP >>= fun sigma ->
   let evdref = ref sigma in
   try
     let _ = Typing.e_sort_of env evdref ty in
@@ -1856,15 +1856,17 @@ let check_decl env decl msg =
     | LocalAssum _ -> ()
     | LocalDef (_,c,_) -> Typing.e_check env evdref c ty
     in
-    Proofview.Unsafe.tclEVARS !evdref
+    !evdref
   with e when Errors.noncritical e ->
-    msg e
+    let id = get_id decl in
+    raise (DependsOnBody (Some id))
 
 let clear_body ids =
   let open Context.Named.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+    let sigma = Tacmach.New.project gl in
     let ctx = named_context env in
     let map = function
     | LocalAssum (id,t) as decl ->
@@ -1878,23 +1880,32 @@ let clear_body ids =
     let ctx = List.map map ctx in
     let base_env = reset_context env in
     let env = push_named_context ctx base_env in
-    let check_hyps =
-      let check env decl =
-        let msg _ = Tacticals.New.tclZEROMSG
-          (str "Hypothesis " ++ pr_id (get_id decl) ++ on_the_bodies ids)
+    let check =
+      try
+        let check (env, sigma) decl =
+          (** Do no recheck hypotheses that do not depend *)
+          let sigma =
+            if List.exists (fun id -> occur_var_in_decl env id decl) ids then
+              check_decl env sigma decl
+            else sigma
+          in
+          (push_named decl env, sigma)
         in
-        check_decl env decl msg <*> Proofview.tclUNIT (push_named decl env)
-      in
-      let checks = Proofview.Monad.List.fold_left check base_env (List.rev ctx) in
-      Proofview.tclIGNORE checks
-    in
-    let check_concl =
-      let msg _ = Tacticals.New.tclZEROMSG
-        (str "Conclusion" ++ on_the_bodies ids)
-      in
-      check_is_type env concl msg
+        let (env, sigma) = List.fold_left check (base_env, sigma) (List.rev ctx) in
+        let sigma =
+          if List.exists (fun id -> occur_var env id concl) ids then
+            check_is_type env sigma concl
+          else sigma
+        in
+        Proofview.Unsafe.tclEVARS sigma
+      with DependsOnBody where ->
+        let msg = match where with
+        | None -> str "Conclusion" ++ on_the_bodies ids
+        | Some id -> str "Hypothesis " ++ pr_id id ++ on_the_bodies ids
+        in
+        Tacticals.New.tclZEROMSG msg
     in
-    check_hyps <*> check_concl <*>
+    check <*>
     Refine.refine ~unsafe:true { run = begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true concl
     end }