Merge branch 'v8.5'

2 files changed, 57 insertions, 13 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index ac41c94646..602917050b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -206,9 +206,47 @@ let rewrite_conv_closed_unif_flags = {
   resolve_evars = false
 }
 
+let rewrite_keyed_core_unif_flags = {
+  modulo_conv_on_closed_terms = Some full_transparent_state;
+    (* We have this flag for historical reasons, it has e.g. the consequence *)
+    (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *)
+
+  use_metas_eagerly_in_conv_on_closed_terms = true;
+  use_evars_eagerly_in_conv_on_closed_terms = false;
+    (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *)
+    (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *)
+
+  modulo_delta = full_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  check_applied_meta_types = true;
+  use_pattern_unification = true;
+    (* To rewrite "?n x y" in "y+x=0" when ?n is *)
+    (* a preexisting evar of the goal*)
+
+  use_meta_bound_pattern_unification = true;
+
+  frozen_evars = Evar.Set.empty;
+    (* This is set dynamically *)
+
+  restrict_conv_on_strict_subterms = false;
+  modulo_betaiota = true;
+  (* Different from conv_closed *)
+  modulo_eta = true;
+}
+
+let rewrite_keyed_unif_flags = {
+  core_unify_flags = rewrite_keyed_core_unif_flags;
+  merge_unify_flags = rewrite_keyed_core_unif_flags;
+  subterm_unify_flags = rewrite_keyed_core_unif_flags;
+  allow_K_in_toplevel_higher_order_unification = false;
+  resolve_evars = false
+}
+
 let rewrite_elim with_evars frzevars cls c e =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_conv_closed_unif_flags c in
+  let flags = if Unification.is_keyed_unification ()
+	      then rewrite_keyed_unif_flags else rewrite_conv_closed_unif_flags in
+  let flags = make_flags frzevars (Tacmach.New.project gl) flags c in
   general_elim_clause with_evars flags cls c e
   end }
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index eddefb2799..1b5525e672 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1525,12 +1525,13 @@ let assert_replacing id newt tac =
 let newfail n s = 
   Proofview.tclZERO (Refiner.FailError (n, lazy s))
 
-let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
+let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
   let treat sigma res = 
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
-    | Some None -> Proofview.tclUNIT ()
+    | Some None -> if progress then newfail 0 (str"Failed to progress")
+		   else Proofview.tclUNIT ()
     | Some (Some res) ->
         let (undef, prf, newt) = res in
         let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
@@ -1597,21 +1598,25 @@ let tactic_init_setoid () =
   try init_setoid (); tclIDTAC
   with e when Errors.noncritical e -> tclFAIL 0 (str"Setoid library not loaded")
 
-(** Setoid rewriting when called with "rewrite_strat" *)
-let cl_rewrite_clause_strat strat clause =
+let cl_rewrite_clause_strat progress strat clause =
   tclTHEN (tactic_init_setoid ())
-  (fun gl -> 
-     try Proofview.V82.of_tactic (cl_rewrite_clause_newtac strat clause) gl
-     with RewriteFailure e ->
-       errorlabstrm "" (str"setoid rewrite failed: " ++ e)
-     | Refiner.FailError (n, pp) -> 
-       tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl)
+  ((if progress then tclWEAK_PROGRESS else fun x -> x)
+   (fun gl -> 
+    try Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~progress strat clause) gl
+    with RewriteFailure e ->
+	 errorlabstrm "" (str"setoid rewrite failed: " ++ e)
+       | Refiner.FailError (n, pp) -> 
+	  tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl))
 
 (** Setoid rewriting when called with "setoid_rewrite" *)
 let cl_rewrite_clause l left2right occs clause gl =
   let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in
-    cl_rewrite_clause_strat strat clause gl
+    cl_rewrite_clause_strat true strat clause gl
 
+(** Setoid rewriting when called with "rewrite_strat" *)
+let cl_rewrite_clause_strat strat clause =
+  cl_rewrite_clause_strat false strat clause
+  
 let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
   let c sigma =
     let (sigma, c) = Pretyping.understand_tcc env sigma c in
@@ -2017,7 +2022,8 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
       tclWEAK_PROGRESS 
 	(tclTHEN
            (Refiner.tclEVARS evd)
-	   (Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~abs:(Some abs) ~origsigma strat cl))) gl
+	   (Proofview.V82.of_tactic
+	    (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) gl
     with RewriteFailure e ->
       tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl