Merge branch 'v8.6' into trunk

6 files changed, 34 insertions, 12 deletions

diff --git a/checker/inductive.ml b/checker/inductive.ml
index cb344c7fd6..c4ffc141ff 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -989,6 +989,10 @@ let check_one_fix renv recpos trees def =
         | (Ind _ | Construct _) ->
             List.iter (check_rec_call renv []) l
 
+	| Proj (p, c) ->
+            List.iter (check_rec_call renv []) l;
+            check_rec_call renv [] c
+
         | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
 
 	| Sort _ -> assert (l = [])
@@ -998,8 +1002,6 @@ let check_one_fix renv recpos trees def =
 
         | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
 
-	| Proj (p, c) -> check_rec_call renv [] c
-
   and check_nested_fix_body renv decr recArgsDecrArg body =
     if decr = 0 then
       check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 2ec6430fdd..a1b3f4f255 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -111,8 +111,8 @@ let declare_tactic loc s c cl = match cl with
   declare_str_items loc
     [ <:str_item< do {
       let obj () = Tacenv.register_ltac True False $name$ $body$ in
-      Tacenv.register_ml_tactic $se$ [|$tac$|];
-      Mltop.declare_cache_obj obj $plugin_name$; } >>
+      let () = Tacenv.register_ml_tactic $se$ [|$tac$|] in
+      Mltop.declare_cache_obj obj $plugin_name$ } >>
     ]
 | _ ->
   (** Otherwise we add parsing and printing rules to generate a call to a
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 7b2d927162..3c4c2796ee 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -990,6 +990,10 @@ let check_one_fix renv recpos trees def =
         | (Ind _ | Construct _) ->
             List.iter (check_rec_call renv []) l
 
+	| Proj (p, c) ->
+           List.iter (check_rec_call renv []) l;
+           check_rec_call renv [] c
+
         | Var id ->
             begin
               let open Context.Named.Declaration in
@@ -1009,8 +1013,6 @@ let check_one_fix renv recpos trees def =
         | (Evar _ | Meta _) -> ()
 
         | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
-	
-	| Proj (p, c) -> check_rec_call renv [] c
 
   and check_nested_fix_body renv decr recArgsDecrArg body =
     if Int.equal decr 0 then
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 0556191be8..e327deda02 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -581,7 +581,7 @@ let general_rewrite_unif_flags () =
   let core_flags =
     { rewrite_core_unif_flags with
       Unification.modulo_conv_on_closed_terms = Some ts;
-      Unification.use_evars_eagerly_in_conv_on_closed_terms = false;
+      Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
       Unification.modulo_delta = ts;
       Unification.modulo_delta_types = ts;
       Unification.modulo_betaiota = true }
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a4bceeb67c..c09693b364 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -211,11 +211,11 @@ GEXTEND Gram
       | IDENT "Conjecture" -> (None, Conjectural) ] ]
   ;
   assumptions_token:
-    [ [ kwd = IDENT "Hypotheses" -> (kwd, (Some Discharge, Logical))
-      | kwd = IDENT "Variables" -> (kwd, (Some Discharge, Definitional))
-      | kwd = IDENT "Axioms" -> (kwd, (None, Logical))
-      | kwd = IDENT "Parameters" -> (kwd, (None, Definitional))
-      | kwd = IDENT "Conjectures" -> (kwd, (None, Conjectural)) ] ]
+    [ [ IDENT "Hypotheses" -> ("Hypotheses", (Some Discharge, Logical))
+      | IDENT "Variables" -> ("Variables", (Some Discharge, Definitional))
+      | IDENT "Axioms" -> ("Axioms", (None, Logical))
+      | IDENT "Parameters" -> ("Parameters", (None, Definitional))
+      | IDENT "Conjectures" -> ("Conjectures", (None, Conjectural)) ] ]
   ;
   inline:
     [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
diff --git a/test-suite/bugs/closed/4679.v b/test-suite/bugs/closed/4679.v
new file mode 100644
index 0000000000..c94fa31a9d
--- /dev/null
+++ b/test-suite/bugs/closed/4679.v
@@ -0,0 +1,18 @@
+Require Import Coq.Setoids.Setoid.
+Goal forall (T : nat -> Set -> Set) (U : Set)
+            (H : forall n : nat, T n (match n with
+                                      | 0 => fun x => x
+                                      | S _ => fun x => x
+                                      end (nat = nat)) = U),
+    T 0 (nat = nat) = U.
+Proof.
+  intros.
+  let H := match goal with H : forall _, eq _ _ |- _ => H end in
+  rewrite H || fail 0 "too early".
+  Undo.
+  let H := match goal with H : forall _, eq _ _ |- _ => H end in
+  setoid_rewrite (H 0) || fail 0 "too early".
+  Undo.
+  setoid_rewrite H. (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. *)
+  reflexivity.
+Qed.
\ No newline at end of file