From b9485da2388e0fe2d634d3359c0504b8c253e554 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 21 Jul 2016 17:03:46 +0200 Subject: Fix bug #4679, weakened setoid_rewrite unification It should use evar instantiations eagerly during unification of the lhs of the lemma, as in 8.4. --- ltac/rewrite.ml | 2 +- test-suite/bugs/closed/4679.v | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4679.v 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/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 -- cgit v1.2.3 From ba00867d515624aee734d998bfbe3880f559d907 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 25 Jul 2016 16:39:34 +0200 Subject: Fix bug #4876: critical bug in guard condition checker. --- checker/inductive.ml | 6 ++++-- kernel/inductive.ml | 6 ++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/checker/inductive.ml b/checker/inductive.ml index 909ecccaed..5825d1ab82 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -988,6 +988,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 = []) @@ -997,8 +1001,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/kernel/inductive.ml b/kernel/inductive.ml index fbe0920bcf..52f578987e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1010,6 +1010,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 match pi2 (lookup_named id renv.env) with @@ -1028,8 +1032,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 -- cgit v1.2.3 From 1ca19082cf506c304b3c7945e72c0238f2aa9d1a Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 26 Jul 2016 14:22:42 +0200 Subject: restore compatibility with gallium's camlp4 (broken by commit 8e07227c) Apparently, in camlp4 (unlike camlp5) : - Something like "[ kwd = IDENT "foobar" -> .... kwd ... ]" produces a kwd of type token instead of string (which sounds reasonable ?). For now, I've replaced kwd by the explicit strings. Not so nice, but works with both camlp4 and camlp5 - A quotation of the form "let obj = ... in bar; baz" is not interpreted in the usual OCaml way, but rather as "(let obj = ... in bar); baz". Let's use instead "let obj = ... in let () = bar in baz", which works fine. --- grammar/tacextend.mlp | 4 ++-- parsing/g_vernac.ml4 | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) 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/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) -- cgit v1.2.3