From ba5c882c6c174170d18fe01f36863ca592065671 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 25 Jul 2016 13:40:41 +0200 Subject: Fix bug #4673: regression in setoid_rewrite. Modulo delta for types should be fully transparent. --- CHANGES | 1 + tactics/rewrite.ml | 2 +- test-suite/bugs/closed/4673.v | 57 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 59 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4673.v diff --git a/CHANGES b/CHANGES index 863c27e477..e6b5b3206e 100644 --- a/CHANGES +++ b/CHANGES @@ -7,6 +7,7 @@ Critical bugfix Other bugfixes - #4780: Induction with universe polymorphism on was creating ill-typed terms. +- #4673: regression in setoid_rewrite, unfolding let-ins for type unification. - #4754: Regression in setoid_rewrite, allow postponed unification problems to remain. - #4769: Anomaly with universe polymorphic schemes defined inside sections. - #3886: Program: duplicate obligations of mutual fixpoints diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 0892dc9e6c..3a62358e3e 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -576,7 +576,7 @@ let general_rewrite_unif_flags () = Unification.modulo_conv_on_closed_terms = Some ts; Unification.use_evars_eagerly_in_conv_on_closed_terms = false; Unification.modulo_delta = ts; - Unification.modulo_delta_types = ts; + Unification.modulo_delta_types = full_transparent_state; Unification.modulo_betaiota = true } in { Unification.core_unify_flags = core_flags; diff --git a/test-suite/bugs/closed/4673.v b/test-suite/bugs/closed/4673.v new file mode 100644 index 0000000000..1ae5081851 --- /dev/null +++ b/test-suite/bugs/closed/4673.v @@ -0,0 +1,57 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerOptimized" "-R" "." "Top") -*- *) +(* File reduced by coq-bug-finder from original input, then from 2407 lines to 22 lines, then from 528 lines to 35 lines, then from 331 lines to 42 lines, then from 56 lines to 42 lines, then from 63 lines to 46 lines, then from 60 lines to 46 lines *) (* coqc version 8.5 (February 2016) compiled on Feb 21 2016 15:26:16 with OCaml 4.02.3 + coqtop version 8.5 (February 2016) *) +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Lists.List. +Import Coq.Lists.List. +Import Coq.Classes.Morphisms. + +Definition list_caset A (P : list A -> Type) (N : P nil) (C : forall x xs, P (x::xs)) + ls + : P ls + := match ls with + | nil => N + | x::xs => C x xs + end. + +Global Instance list_caset_Proper' {A P} + : Proper (eq + ==> pointwise_relation _ (pointwise_relation _ eq) + ==> eq + ==> eq) + (@list_caset A (fun _ => P)). +admit. +Defined. + +Global Instance list_caset_Proper'' {A P} + : (Proper (eq ==> pointwise_relation _ (pointwise_relation _ eq) ==> forall_relation (fun _ => eq)) + (list_caset A (fun _ => P))). +Admitted. + +Goal forall (Char : Type) (P : forall _ : list bool, Prop) (l : list bool) (l0 : forall _ : forall _ : Char, bool, list bool) + + (T : Type) (T0 : forall _ : T, Type) (t : T), + + let predata := t in + + forall (splitdata : T0 predata) (l5 : forall _ : T0 t, list nat) (T1 : Type) (b : forall (_ : T1) (_ : Char), bool) + + (T2 : Type) (a11 : T2) (xs : list T2) (T3 : Type) (i0 : T3) (P0 : Set) (b1 : forall (_ : nat) (_ : P0), bool) + + (l2 : forall (_ : forall _ : T1, list bool) (_ : forall _ : P0, list bool) (_ : T2), list bool) + + (l1 : forall (_ : forall _ : forall _ : Char, bool, list bool) (_ : forall _ : P0, list bool) (_ : T3), list bool) + + (_ : forall NT : forall _ : P0, list bool, @eq (list bool) (l1 l0 NT i0) (l2 (fun f : T1 => l0 (b f)) NT a11)), + + P + (@list_caset T2 (fun _ : list T2 => list bool) l + (fun (_ : T2) (_ : list T2) => l1 l0 (fun a9 : P0 => @map nat bool (fun x0 : nat => b1 x0 a9) (l5 splitdata)) i0 +) xs). + intros. + subst predata; + let H := match goal with H : forall _, _ = _ |- _ => H end in + setoid_rewrite H || fail 0 "too early". + Undo. + setoid_rewrite H. -- cgit v1.2.3 From 09018d8a3ca4a1b1b69d4baa911ac8e4f09b55e6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 4 Aug 2016 08:00:05 +0200 Subject: Fix documentation typo (bug #4994). --- doc/refman/RefMan-oth.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 0a243308d5..ddbe0bbb31 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -87,7 +87,7 @@ is restored when the current \emph{section} ends. \item {\tt Global Unset {\rm\sl flag}.\comindex{Global Unset}}\\ This command switches {\rm\sl flag} off. The original state of {\rm\sl flag} is \emph{not} restored at the end of the module. Additionally, -if set in a file, {\rm\sl flag} is switched on when the file is +if set in a file, {\rm\sl flag} is switched off when the file is {\tt Require}-d. \end{Variants} -- cgit v1.2.3 From 2f26c2fd368a10b89273712e3de64bbd83aedc59 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 7 Aug 2016 23:56:32 +0200 Subject: Fix #5000: Document the native compiler soundness bug due to Unicode mangling. --- CHANGES | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGES b/CHANGES index e6b5b3206e..c74aa7234c 100644 --- a/CHANGES +++ b/CHANGES @@ -17,6 +17,8 @@ Changes from V8.5pl1 to V8.5pl2 Critical bugfix - Checksums of .vo files dependencies were not correctly checked. +- Unicode-to-ASCII translation was not injective, leading in a soundness bug in + the native compiler. Other bugfixes -- cgit v1.2.3 From e154bf3505658b59c1cce53bd3061586bc353449 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 11 Aug 2016 09:30:34 +0200 Subject: Use the "md5" command on OpenBSD (bug #5008). --- configure.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index 6748da1d84..5b4ab883df 100644 --- a/configure.ml +++ b/configure.ml @@ -827,7 +827,8 @@ let strip = (** * md5sum command *) let md5sum = - if arch = "Darwin" || arch = "FreeBSD" then "md5 -q" else "md5sum" + if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"] + then "md5 -q" else "md5sum" (** * Documentation : do we have latex, hevea, ... *) -- cgit v1.2.3 From c90c53129436014b0020c52641277d616144282a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 11 Aug 2016 09:37:29 +0200 Subject: Do not assume the "TERM" environment variable is always set (bug #5007). --- toplevel/coqtop.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 9e1a76bbd6..3d5080177c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -55,7 +55,7 @@ let init_color () = Terminal.has_style Unix.stderr && (* emacs compilation buffer does not support colors by default, its TERM variable is set to "dumb". *) - Unix.getenv "TERM" <> "dumb" + try Sys.getenv "TERM" <> "dumb" with Not_found -> false in if has_color then begin let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in -- cgit v1.2.3 From 6d1e0f80d215678559ada3d5b32c22c0d015454e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 14 Aug 2016 18:03:22 +0200 Subject: Fix regression in Coqide's "forward one command" command In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".". In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed. I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command". --- ide/coqOps.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 80ce99a69e..e12fda9141 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -338,8 +338,11 @@ object(self) method private show_goals_aux ?(move_insert=false) () = Coq.PrintOpt.set_printing_width proof#width; if move_insert then begin - buffer#place_cursor ~where:self#get_start_of_input; - script#recenter_insert; + let dest = self#get_start_of_input in + if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin + buffer#place_cursor ~where:dest; + script#recenter_insert + end end; Coq.bind (Coq.goals ~logger:messages#push ()) (function | Fail x -> self#handle_failure_aux ~move_insert x -- cgit v1.2.3