diff options
42 files changed, 180 insertions, 91 deletions
@@ -15,10 +15,7 @@ Tactics profiling, and "Set NativeCompute Profile Filename" customizes the profile filename. - The tactic "omega" is now aware of the bodies of context variables - such as "x := 5 : Z" (see bug #148). This could be disabled via - Unset Omega UseLocalDefs. -- The tactic "omega" is now aware of the bodies of context variables - such as "x := 5 : Z" (see bug #148). This could be disabled via + such as "x := 5 : Z" (see BZ#148). This could be disabled via Unset Omega UseLocalDefs. - The tactic "romega" is also aware now of the bodies of context variables. @@ -2397,7 +2394,7 @@ Tactics a registered setoid equality before starting to reduce in H. This is unlikely to break any script. Should this happen nonetheless, one can insert manually some "unfold ... in H" before rewriting. -- Fixed various bugs about (setoid) rewrite ... in ... (in particular #1101) +- Fixed various bugs about (setoid) rewrite ... in ... (in particular BZ#1101) - "rewrite ... in" now accepts a clause as place where to rewrite instead of juste a simple hypothesis name. For instance: rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H @@ -2974,11 +2971,11 @@ Incompatibilities Bugs - Improved localisation of errors in Syntactic Definitions -- Induction principle creation failure in presence of let-in fixed (#238) -- Inversion bugs fixed (#212 and #220) -- Omega bug related to Set fixed (#180) -- Type-checking inefficiency of nested destructuring let-in fixed (#216) -- Improved handling of let-in during holes resolution phase (#239) +- Induction principle creation failure in presence of let-in fixed (BZ#238) +- Inversion bugs fixed (BZ#212 and BZ#220) +- Omega bug related to Set fixed (BZ#180) +- Type-checking inefficiency of nested destructuring let-in fixed (BZ#216) +- Improved handling of let-in during holes resolution phase (BZ#239) Efficiency @@ -2991,18 +2988,18 @@ Changes from V7.3 to V7.3.1 Bug fixes - Corrupted Field tactic and Match Context tactic construction fixed - - Checking of names already existing in Assert added (PR#182) - - Invalid argument bug in Exact tactic solved (PR#183) - - Colliding bound names bug fixed (PR#202) - - Wrong non-recursivity test for Record fixed (PR#189) - - Out of memory/seg fault bug related to parametric inductive fixed (PR#195) + - Checking of names already existing in Assert added (BZ#182) + - Invalid argument bug in Exact tactic solved (BZ#183) + - Colliding bound names bug fixed (BZ#202) + - Wrong non-recursivity test for Record fixed (BZ#189) + - Out of memory/seg fault bug related to parametric inductive fixed (BZ#195) - Setoid_replace/Setoid_rewrite bug wrt "==" fixed Misc - Ocaml version >= 3.06 is needed to compile Coq from sources - Simplification of fresh names creation strategy for Assert, Pose and - LetTac (PR#192) + LetTac (BZ#192) Changes from V7.2 to V7.3 ========================= diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index c935b6b140..2bc3370286 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -4,13 +4,13 @@ Thank you for your interest in contributing to Coq! There are many ways to contr ## Bug Reports -Bug reports are enormously useful to identify issues with Coq; we can't fix what we don't know about. Bug reports should all be filed on the [Coq Bugzilla](https://coq.inria.fr/bugs/) (you'll have to make an account). You can file a bug for any of the following: +Bug reports are enormously useful to identify issues with Coq; we can't fix what we don't know about. To report a bug, please open an issue on the [Coq GitHub repository](https://github.com/coq/coq/issues) (you'll need a GitHub account). You can file a bug for any of the following: - An anomaly. These are always considered bugs, so Coq will even ask you to file a bug report! - An error you didn't expect. If you're not sure whether it's a bug or intentional, feel free to file a bug anyway. We may want to improve the documentation or error message. - Missing documentation. It's helpful to track where the documentation should be improved, so please file a bug if you can't find or don't understand some bit of documentation. - An error message that wasn't as helpful as you'd like. Bonus points for suggesting what information would have helped you. -- Bugs in CoqIDE should also be filed on the Bugzilla. Bugs in the Emacs plugin should be filed against [ProofGeneral](https://github.com/ProofGeneral/PG/issues), or against [company-coq](https://github.com/cpitclaudel/company-coq/issues) if they are specific to company-coq features. +- Bugs in CoqIDE should also be filed on the [GitHub issue tracker](https://github.com/coq/coq/issues). Bugs in the Emacs plugin should be filed against [ProofGeneral](https://github.com/ProofGeneral/PG/issues), or against [company-coq](https://github.com/cpitclaudel/company-coq/issues) if they are specific to company-coq features. It would help if you search the existing issues before reporting a bug. This can be difficult, so consider it extra credit. We don't mind duplicate bug reports. @@ -40,7 +40,7 @@ Here are a few tags Coq developers may add to your PR and what they mean. In gen Currently the process for contributing to the documentation is the same as for changing anything else in Coq, so please submit a pull request as described above. -Bugzilla includes a component to mark bugs related to documentation. You can view a list of documentation-related bugs using a [Bugzilla search](https://coq.inria.fr/bugs/buglist.cgi?component=Doc&list_id=455006&product=Coq&resolution=---). Many of these bugs can be fixed by contributing writing, without knowledge of Coq's OCaml source code. +Our issue tracker includes a flag to mark bugs related to documentation. You can view a list of documentation-related bugs using a [GitHub issue search](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Aissue%20label%3A%22kind%3A%20documentation%22%20). Many of these bugs can be fixed by contributing writing, without knowledge of Coq's OCaml source code. The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) are at [`doc/refman`](/doc/refman). These are written in LaTeX and compiled to HTML with [HeVeA](http://hevea.inria.fr/). diff --git a/ISSUE_TEMPLATE.md b/ISSUE_TEMPLATE.md new file mode 100644 index 0000000000..c9cb516cd3 --- /dev/null +++ b/ISSUE_TEMPLATE.md @@ -0,0 +1,18 @@ +<!-- Thank you for your contribution. + Please complete the following information when reporting a bug. --> + +#### Version + +<!-- You can get this information by running `coqtop -v`. --> + + +#### Operating system + + +#### Description of the problem + +<!-- It is helpful to provide enough information so that we can reproduce the bug. + In particular, please include a code example which produces it. + If the example is small, you can include it here between ``` ```. + Otherwise, please provide a link to a repository, a gist (https://gist.github.com) + or drag-and-drop a `.zip` archive. --> @@ -42,7 +42,7 @@ For any questions/suggestions about the Coq Club, please write to `coq-club-request@inria.fr`. ## Bugs report -Send your bug reports by filling a form at [coq.inria.fr/bugs](http://coq.inria.fr/bugs). +Please report any bug in [our issue tracker](https://github.com/coq/coq/issues). To be effective, bug reports should mention the OCaml version used to compile and run Coq, the Coq version (`coqtop -v`), the configuration diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES index cf97ae3ab8..4bc3dba36e 100644 --- a/plugins/extraction/CHANGES +++ b/plugins/extraction/CHANGES @@ -54,7 +54,7 @@ but also a few steps toward a more user-friendly extraction: * bug fixes: - many concerning Records. -- a Stack Overflow with mutual inductive (PR#320) +- a Stack Overflow with mutual inductive (BZ#320) - some optimizations have been removed since they were not type-safe: For example if e has type: type 'x a = A Then: match e with A -> A -----X----> e @@ -125,7 +125,7 @@ but also a few steps toward a more user-friendly extraction: - the dummy constant "__" have changed. see README - - a few bug-fixes (#191 and others) + - a few bug-fixes (BZ#191 and others) 7.2 -> 7.3 diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 0f537abece..f708307c38 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -145,7 +145,7 @@ let rec pp_expr par env args = | MLrel n -> let id = get_db_name n env in (* Try to survive to the occurrence of a Dummy rel. - TODO: we should get rid of this hack (cf. #592) *) + TODO: we should get rid of this hack (cf. BZ#592) *) let id = if Id.equal id dummy_name then Id.of_string "__" else id in apply (Id.print id) | MLapp (f,args') -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cb76df4e8a..0f1a508c8d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -176,6 +176,12 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let s = ESorts.kind sigma s in lookup_canonical_conversion (proji, Sort_cs (family_of_sort s)),[] + | Proj (p, c) -> + let c2 = Globnames.ConstRef (Projection.constant p) in + let c = Retyping.expand_projection env sigma p c [] in + let _, args = destApp sigma c in + let sk2 = Stack.append_app args sk2 in + lookup_canonical_conversion (proji, Const_cs c2), sk2 | _ -> let (c2, _) = Termops.global_of_constr sigma t2 in lookup_canonical_conversion (proji, Const_cs c2),sk2 diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index a23579609a..e970a1db90 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -171,7 +171,7 @@ let keep_true_projections projs kinds = let filter (p, (_, b)) = if b then Some p else None in List.map_filter filter (List.combine projs kinds) -let cs_pattern_of_constr t = +let cs_pattern_of_constr env t = match kind_of_term t with App (f,vargs) -> begin @@ -180,6 +180,10 @@ let cs_pattern_of_constr t = end | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] + | Proj (p, c) -> + let { Environ.uj_type = ty } = Typeops.infer env c in + let _, params = Inductive.find_rectype env ty in + Const_cs (ConstRef (Projection.constant p)), None, params @ [c] | Sort s -> Sort_cs (family_of_sort s), None, [] | _ -> begin @@ -190,7 +194,6 @@ let cs_pattern_of_constr t = let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" (fun (sign,env,t,con,proji_sp) -> - let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let env = Termops.push_rels_assum sign env in let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in @@ -207,14 +210,16 @@ let compute_canonical_projections warn (con,ind) = let v = (mkConstU (con,u)) in let c = Environ.constant_value_in env (con,u) in let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in + let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in - let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in + let lt = List.rev_map snd sign in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in let params, projs = List.chop p args in let lpj = keep_true_projections lpj kl in let lps = List.combine lpj projs in + let nenv = Termops.push_rels_assum sign env in let comp = List.fold_left (fun l (spopt,t) -> (* comp=components *) @@ -222,7 +227,7 @@ let compute_canonical_projections warn (con,ind) = | Some proji_sp -> begin try - let patt, n , args = cs_pattern_of_constr t in + let patt, n , args = cs_pattern_of_constr nenv t in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp); @@ -324,15 +329,25 @@ let declare_canonical_structure ref = let lookup_canonical_conversion (proj,pat) = assoc_pat pat (Refmap.find proj !object_table) +let decompose_projection sigma c args = + match EConstr.kind sigma c with + | Const (c, u) -> + let n = find_projection_nparams (ConstRef c) in + (** Check if there is some canonical projection attached to this structure *) + let _ = Refmap.find (ConstRef c) !object_table in + let arg = Stack.nth args n in + arg + | Proj (p, c) -> + let _ = Refmap.find (ConstRef (Projection.constant p)) !object_table in + c + | _ -> raise Not_found + let is_open_canonical_projection env sigma (c,args) = let open EConstr in try - let (ref, _) = Termops.global_of_constr sigma c in - let n = find_projection_nparams ref in - (** Check if there is some canonical projection attached to this structure *) - let _ = Refmap.find ref !object_table in + let arg = decompose_projection sigma c args in try - let arg = whd_all env sigma (Stack.nth args n) in + let arg = whd_all env sigma arg in let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in not (isConstruct sigma hd) with Failure _ -> false diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 5480b14af0..8e2333b349 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -65,7 +65,7 @@ type obj_typ = { o_TCOMPS : constr list } (** ordered *) (** Return the form of the component of a canonical structure *) -val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list +val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * constr list val pr_cs_pattern : cs_pattern -> Pp.t diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d52c3932df..e8f7e2bbaf 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -501,6 +501,10 @@ let expand_key ts env sigma = function in if EConstr.eq_constr sigma (EConstr.mkProj (p, c)) red then None else Some red | None -> None +let isApp_or_Proj sigma c = + match kind sigma c with + | App _ | Proj _ -> true + | _ -> false type unirec_flags = { at_top: bool; @@ -1020,7 +1024,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) = let f1 () = - if isApp sigma cM then + if isApp_or_Proj sigma cM then let f1l1 = whd_nored_state sigma (cM,Stack.empty) in if is_open_canonical_projection curenv sigma f1l1 then let f2l2 = whd_nored_state sigma (cN,Stack.empty) in @@ -1036,7 +1040,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e error_cannot_unify (fst curenvnb) sigma (cM,cN) else try f1 () with e when precatchable_exception e -> - if isApp sigma cN then + if isApp_or_Proj sigma cN then let f2l2 = whd_nored_state sigma (cN, Stack.empty) in if is_open_canonical_projection curenv sigma f2l2 then let f1l1 = whd_nored_state sigma (cM, Stack.empty) in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6f7e61f6ba..e8a78d72d6 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2471,7 +2471,7 @@ let exceed_bound n = function (* We delay thinning until the completion of the whole intros tactic to ensure that dependent hypotheses are cleared in the right - dependency order (see bug #1000); we use fresh names, not used in + dependency order (see BZ#1000); we use fresh names, not used in the tactic, for the hyps to clear *) (* In [intro_patterns_core b avoid ids thin destopt bound n tac patl]: [b]: compatibility flag, if false at toplevel, do not complete incomplete diff --git a/test-suite/bugs/closed/5692.v b/test-suite/bugs/closed/5692.v index 55ef7abe40..4c8d464f19 100644 --- a/test-suite/bugs/closed/5692.v +++ b/test-suite/bugs/closed/5692.v @@ -1,9 +1,59 @@ Set Primitive Projections. Require Import ZArith ssreflect. -Module Test3. +Module Test1. -Set Primitive Projections. +Structure semigroup := SemiGroup { + sg_car :> Type; + sg_op : sg_car -> sg_car -> sg_car; +}. + +Structure monoid := Monoid { + monoid_car :> Type; + monoid_op : monoid_car -> monoid_car -> monoid_car; + monoid_unit : monoid_car; +}. + +Coercion monoid_sg (X : monoid) : semigroup := + SemiGroup (monoid_car X) (monoid_op X). +Canonical Structure monoid_sg. + +Parameter X : monoid. +Parameter x y : X. + +Check (sg_op _ x y). + +End Test1. + +Module Test2. + +Structure semigroup := SemiGroup { + sg_car :> Type; + sg_op : sg_car -> sg_car -> sg_car; +}. + +Structure monoid := Monoid { + monoid_car :> Type; + monoid_op : monoid_car -> monoid_car -> monoid_car; + monoid_unit : monoid_car; + monoid_left_id x : monoid_op monoid_unit x = x; +}. + +Coercion monoid_sg (X : monoid) : semigroup := + SemiGroup (monoid_car X) (monoid_op X). +Canonical Structure monoid_sg. + +Canonical Structure nat_sg := SemiGroup nat plus. +Canonical Structure nat_monoid := Monoid nat plus 0 plus_O_n. + +Lemma foo (x : nat) : 0 + x = x. +Proof. +apply monoid_left_id. +Qed. + +End Test2. + +Module Test3. Structure semigroup := SemiGroup { sg_car :> Type; diff --git a/test-suite/ideal-features/complexity/evars_subst.v b/test-suite/ideal-features/complexity/evars_subst.v index b3dfb33cdc..b9c3598887 100644 --- a/test-suite/ideal-features/complexity/evars_subst.v +++ b/test-suite/ideal-features/complexity/evars_subst.v @@ -1,4 +1,4 @@ -(* Bug report #932 *) +(* BZ#932 *) (* Expected time < 1.00s *) (* Let n be the number of let-in. The complexity comes from the fact diff --git a/test-suite/ideal-features/evars_subst.v b/test-suite/ideal-features/evars_subst.v index b3dfb33cdc..b9c3598887 100644 --- a/test-suite/ideal-features/evars_subst.v +++ b/test-suite/ideal-features/evars_subst.v @@ -1,4 +1,4 @@ -(* Bug report #932 *) +(* BZ#932 *) (* Expected time < 1.00s *) (* Let n be the number of let-in. The complexity comes from the fact diff --git a/test-suite/interactive/Back.v b/test-suite/interactive/Back.v index b813a79ab2..22364254dc 100644 --- a/test-suite/interactive/Back.v +++ b/test-suite/interactive/Back.v @@ -1,5 +1,5 @@ (* Check that reset remains synchronised with the compilation unit cache *) -(* See bug #1030 *) +(* See BZ#1030 *) Section multiset_defs. Require Import Plus. diff --git a/test-suite/modules/objects2.v b/test-suite/modules/objects2.v index 220e2b3694..0a6b1f06de 100644 --- a/test-suite/modules/objects2.v +++ b/test-suite/modules/objects2.v @@ -2,7 +2,7 @@ the logical objects in the environment *) -(* Bug #1118 (simplified version), submitted by Evelyne Contejean +(* BZ#1118 (simplified version), submitted by Evelyne Contejean (used to failed in pre-V8.1 trunk because of a call to lookup_mind for structure objects) *) diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index fafb478bad..61ae4edbd1 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -7,7 +7,7 @@ Check | a :: l => f a :: F _ _ f l end). -(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf bug #860) *) +(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf BZ#860) *) Check let fix f (m : nat) : nat := match m with diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index 7c9b89f9d2..306532c0df 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -1,7 +1,7 @@ Set Implicit Arguments. Unset Strict Implicit. -(* Suggested by Pierre Casteran (bug #169) *) +(* Suggested by Pierre Casteran (BZ#169) *) (* Argument 3 is needed to typecheck and should be printed *) Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x). Check (compose (C:=nat) S). diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index 9a5edb813d..75b66e463a 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -7,12 +7,12 @@ Ltac f H := split; [a H|e H]. Print Ltac f. (* Test printing of match context *) -(* Used to fail after translator removal (see bug #1070) *) +(* Used to fail after translator removal (see BZ#1070) *) Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end. Print Ltac g. -(* Test an error message (#5390) *) +(* Test an error message (BZ#5390) *) Lemma myid (P : Prop) : P <-> P. Proof. split; auto. Qed. diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v index 69dc9aca78..d52a853aae 100644 --- a/test-suite/success/Abstract.v +++ b/test-suite/success/Abstract.v @@ -1,4 +1,4 @@ -(* Cf coqbugs #546 *) +(* Cf BZ#546 *) Require Import Omega. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 06f807f29a..893d75b77f 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -64,7 +64,7 @@ Check (fun x:I1 => end). (* Check implicit parameters of inductive types (submitted by Pierre - Casteran and also implicit in #338) *) + Casteran and also implicit in BZ#338) *) Set Implicit Arguments. Unset Strict Implicit. @@ -80,7 +80,7 @@ Inductive Finite (A : Set) : LList A -> Prop := | Finite_LCons : forall (a : A) (l : LList A), Finite l -> Finite (LCons a l). -(* Check positivity modulo reduction (cf bug #983) *) +(* Check positivity modulo reduction (cf bug BZ#983) *) Record P:Type := {PA:Set; PB:Set}. diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 850f094348..45c71615fc 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -1,6 +1,6 @@ Axiom magic : False. -(* Submitted by Dachuan Yu (bug #220) *) +(* Submitted by Dachuan Yu (BZ#220) *) Fixpoint T (n : nat) : Type := match n with | O => nat -> Prop @@ -16,7 +16,7 @@ Lemma Inversion_RO : forall l : nat, R 0 Psi0 l -> Psi00 l. inversion 1. Abort. -(* Submitted by Pierre Casteran (bug #540) *) +(* Submitted by Pierre Casteran (BZ#540) *) Set Implicit Arguments. Unset Strict Implicit. @@ -64,7 +64,7 @@ elim magic. elim magic. Qed. -(* Submitted by Boris Yakobowski (bug #529) *) +(* Submitted by Boris Yakobowski (BZ#529) *) (* Check that Inversion does not fail due to unnormalized evars *) Set Implicit Arguments. @@ -100,7 +100,7 @@ intros a b H. inversion H. Abort. -(* Check non-regression of bug #1968 *) +(* Check non-regression of BZ#1968 *) Inductive foo2 : option nat -> Prop := Foo : forall t, foo2 (Some t). Goal forall o, foo2 o -> 0 = 1. @@ -130,7 +130,7 @@ Proof. intros. inversion H. Abort. -(* Bug #2314 (simplified): check that errors do not show as anomalies *) +(* BZ#2314 (simplified): check that errors do not show as anomalies *) Goal True -> True. intro. @@ -158,7 +158,7 @@ reflexivity. Qed. (* Up to September 2014, Mapp below was called MApp0 because of a bug - in intro_replacing (short version of bug 2164.v) + in intro_replacing (short version of BZ#2164.v) (example taken from CoLoR) *) Parameter Term : Type. diff --git a/test-suite/success/Mod_type.v b/test-suite/success/Mod_type.v index d5e1a38cf5..6c59bf6edb 100644 --- a/test-suite/success/Mod_type.v +++ b/test-suite/success/Mod_type.v @@ -1,4 +1,4 @@ -(* Check bug #1025 submitted by Pierre-Luc Carmel Biron *) +(* Check BZ#1025 submitted by Pierre-Luc Carmel Biron *) Module Type FOO. Parameter A : Type. @@ -18,7 +18,7 @@ Module Bar : BAR. End Bar. -(* Check bug #2809: correct printing of modules with notations *) +(* Check BZ#2809: correct printing of modules with notations *) Module C. Inductive test : Type := diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 4d04f2cf9b..e3f90f6d94 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -1,5 +1,5 @@ (* Check that "where" clause behaves as if given independently of the *) -(* definition (variant of bug #1132 submitted by Assia Mahboubi) *) +(* definition (variant of BZ#1132 submitted by Assia Mahboubi) *) Fixpoint plus1 (n m:nat) {struct n} : nat := match n with diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index ecbf04e412..470e4f0580 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -52,7 +52,7 @@ Lemma lem5 : (H > 0)%Z. Qed. End B. -(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *) +(* From Nicolas Oury (BZ#180): handling -> on Set (fixed Oct 2002) *) Lemma lem6 : forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. intros. @@ -86,7 +86,7 @@ intros; omega. Qed. (* Check that the interpretation of mult on nat enforces its positivity *) -(* Submitted by Hubert Thierry (bug #743) *) +(* Submitted by Hubert Thierry (BZ#743) *) (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) Lemma lem10 : forall n m:nat, le n (plus n (mult n m)). Proof. diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v index b8f8660e9c..6fd936935c 100644 --- a/test-suite/success/Omega0.v +++ b/test-suite/success/Omega0.v @@ -132,7 +132,7 @@ intros. omega. Qed. -(* Magaud #240 *) +(* Magaud BZ#240 *) Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. intros. diff --git a/test-suite/success/Omega2.v b/test-suite/success/Omega2.v index c4d086a348..4e726335c9 100644 --- a/test-suite/success/Omega2.v +++ b/test-suite/success/Omega2.v @@ -1,6 +1,6 @@ Require Import ZArith Omega. -(* Submitted by Yegor Bryukhov (#922) *) +(* Submitted by Yegor Bryukhov (BZ#922) *) Open Scope Z_scope. diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v index 801ece9e3d..0df3d5685d 100644 --- a/test-suite/success/ROmega.v +++ b/test-suite/success/ROmega.v @@ -52,7 +52,7 @@ Lemma lem5 : (H > 0)%Z. Qed. End B. -(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *) +(* From Nicolas Oury (BZ#180): handling -> on Set (fixed Oct 2002) *) Lemma lem6 : forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. intros. @@ -88,7 +88,7 @@ romega with nat. Qed. (* Check that the interpretation of mult on nat enforces its positivity *) -(* Submitted by Hubert Thierry (bug #743) *) +(* Submitted by Hubert Thierry (BZ#743) *) (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) Lemma lem10 : forall n m : nat, le n (plus n (mult n m)). Proof. diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v index 42730f2e16..3ddf6a40fb 100644 --- a/test-suite/success/ROmega0.v +++ b/test-suite/success/ROmega0.v @@ -132,7 +132,7 @@ intros. romega. Qed. -(* Magaud #240 *) +(* Magaud BZ#240 *) Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. Proof. @@ -146,7 +146,7 @@ intros x y. romega. Qed. -(* Besson #1298 *) +(* Besson BZ#1298 *) Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False. Proof. diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v index 87e8c8e33e..43eda67ea3 100644 --- a/test-suite/success/ROmega2.v +++ b/test-suite/success/ROmega2.v @@ -1,6 +1,6 @@ Require Import ZArith ROmega. -(* Submitted by Yegor Bryukhov (#922) *) +(* Submitted by Yegor Bryukhov (BZ#922) *) Open Scope Z_scope. diff --git a/test-suite/success/Rename.v b/test-suite/success/Rename.v index 0576f3c68f..2789c6c9a6 100644 --- a/test-suite/success/Rename.v +++ b/test-suite/success/Rename.v @@ -4,7 +4,7 @@ rename n into p. induction p; auto. Qed. -(* Submitted by Iris Loeb (#842) *) +(* Submitted by Iris Loeb (BZ#842) *) Section rename. diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v index 361c787e25..76aac39a55 100644 --- a/test-suite/success/Try.v +++ b/test-suite/success/Try.v @@ -1,5 +1,5 @@ (* To shorten interactive scripts, it is better that Try catches - non-existent names in Unfold [cf bug #263] *) + non-existent names in Unfold [cf BZ#263] *) Lemma lem1 : True. try unfold i_dont_exist. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 90a60daa66..0219c3bfdf 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -12,7 +12,7 @@ assumption. assumption. Qed. -(* Simplification of bug 711 *) +(* Simplification of BZ#711 *) Parameter f : true = false. Goal let p := f in True. @@ -37,7 +37,7 @@ Goal True. case Refl || ecase Refl. Abort. -(* Submitted by B. Baydemir (bug #1882) *) +(* Submitted by B. Baydemir (BZ#1882) *) Require Import List. @@ -385,7 +385,7 @@ intros. Fail destruct H. Abort. -(* Check keep option (bug #3791) *) +(* Check keep option (BZ#3791) *) Goal forall b:bool, True. intro b. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index c36313ec16..627794832d 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -23,7 +23,7 @@ Definition f1 frm0 a1 : B := f frm0 a1. (* Checks that solvable ? in the type part of the definition are harmless *) Definition f2 frm0 a1 : B := f frm0 a1. -(* Checks that sorts that are evars are handled correctly (bug 705) *) +(* Checks that sorts that are evars are handled correctly (BZ#705) *) Require Import List. Fixpoint build (nl : list nat) : @@ -58,7 +58,7 @@ Check (forall y n : nat, {q : nat | y = q * n}) -> forall n : nat, {q : nat | x = q * n}). -(* Check instantiation of nested evars (bug #1089) *) +(* Check instantiation of nested evars (BZ#1089) *) Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))). @@ -188,7 +188,7 @@ Abort. End Additions_while. -(* Two examples from G. Melquiond (bugs #1878 and #1884) *) +(* Two examples from G. Melquiond (BZ#1878 and BZ#1884) *) Parameter F1 G1 : nat -> Prop. Goal forall x : nat, F1 x -> G1 x. @@ -207,7 +207,7 @@ Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) := | (existT _ k v)::l' => (existT _ k v):: (filter A l') end. -(* Bug #2000: used to raise Out of memory in 8.2 while it should fail by +(* BZ#2000: used to raise Out of memory in 8.2 while it should fail by lack of information on the conclusion of the type of j *) Goal True. @@ -381,7 +381,7 @@ Section evar_evar_occur. Check match g _ with conj a b => f _ a b end. End evar_evar_occur. -(* Eta expansion (bug #2936) *) +(* Eta expansion (BZ#2936) *) Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }. Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri { tri0 : forall a b c, R a b -> S a c -> T b c diff --git a/test-suite/success/if.v b/test-suite/success/if.v index 9fde95e80d..c81d2b9bf1 100644 --- a/test-suite/success/if.v +++ b/test-suite/success/if.v @@ -3,7 +3,7 @@ Check (fun b : bool => if b then Type else nat). -(* Check correct use of if-then-else predicate annotation (cf bug 690) *) +(* Check correct use of if-then-else predicate annotation (cf BZ#690) *) Check fun b : bool => if b as b0 return (if b0 then b0 = true else b0 = false) diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index ee69df9774..a329894aad 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -1,5 +1,5 @@ (* Thinning introduction hypothesis must be done after all introductions *) -(* Submitted by Guillaume Melquiond (bug #1000) *) +(* Submitted by Guillaume Melquiond (BZ#1000) *) Goal forall A, A -> True. intros _ _. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 29e373eaa5..0f22a1f0a0 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -147,7 +147,7 @@ check_binding ipattern:(H). Abort. (* Check that variables explicitly parsed as ltac variables are not - seen as intro pattern or constr (bug #984) *) + seen as intro pattern or constr (BZ#984) *) Ltac afi tac := intros; tac. Goal 1 = 2. diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 352abb2af5..b8a8ff7561 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -31,7 +31,7 @@ Proof. end). Abort. -(* Submitted by Roland Zumkeller (bug #888) *) +(* Submitted by Roland Zumkeller (BZ#888) *) (* The Fix and CoFix rules expect a subgoal even for closed components of the (co-)fixpoint *) @@ -43,7 +43,7 @@ Goal nat -> nat. exact 0. Qed. -(* Submitted by Roland Zumkeller (bug #889) *) +(* Submitted by Roland Zumkeller (BZ#889) *) (* The types of metas were in metamap and they were not updated when passing through a binder *) @@ -56,7 +56,7 @@ Goal forall n : nat, nat -> n = 0. end). Abort. -(* Submitted by Roland Zumkeller (bug #931) *) +(* Submitted by Roland Zumkeller (BZ#931) *) (* Don't turn dependent evar into metas *) Goal (forall n : nat, n = 0 -> Prop) -> Prop. @@ -65,7 +65,7 @@ intro P. reflexivity. Abort. -(* Submitted by Jacek Chrzaszcz (bug #1102) *) +(* Submitted by Jacek Chrzaszcz (BZ#1102) *) (* le problème a été résolu ici par normalisation des evars présentes dans les types d'evars, mais le problème reste a priori ouvert dans diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v index 5b87e877bf..1bfb8580b3 100644 --- a/test-suite/success/simpl.v +++ b/test-suite/success/simpl.v @@ -1,6 +1,6 @@ Require Import TestSuite.admit. (* Check that inversion of names of mutual inductive fixpoints works *) -(* (cf bug #1031) *) +(* (cf BZ#1031) *) Inductive tree : Set := | node : nat -> forest -> tree diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 6f7498d659..1ffc026730 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -43,7 +43,7 @@ Check (fun _h1 => (zenon_notall nat _ (fun _T_0 => (fun _h2 => (zenon_noteq _ _T_0 _h2))) _h1)). -(* Core of an example submitted by Ralph Matthes (#849) +(* Core of an example submitted by Ralph Matthes (BZ#849) It used to fail because of the K-variable x in the type of "sum_rec ..." which was not in the scope of the evar ?B. Solved by a head @@ -131,7 +131,7 @@ try case nonemptyT_intro. (* check that it fails w/o anomaly *) Abort. (* Test handling of return type and when it is decided to make the - predicate dependent or not - see "bug" #1851 *) + predicate dependent or not - see "bug" BZ#1851 *) Goal forall X (a:X) (f':nat -> X), (exists f : nat -> X, True). intros. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index fc74225d76..2863404590 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -20,8 +20,7 @@ intro P; pattern P. apply lem2. Abort. -(* Check managing of universe constraints in inversion *) -(* Bug report #855 *) +(* Check managing of universe constraints in inversion (BZ#855) *) Inductive dep_eq : forall X : Type, X -> X -> Prop := | intro_eq : forall (X : Type) (f : X), dep_eq X f f @@ -40,7 +39,7 @@ Proof. Abort. -(* Submitted by Bas Spitters (bug report #935) *) +(* Submitted by Bas Spitters (BZ#935) *) (* This is a problem with the status of the type in LetIn: is it a user-provided one or an inferred one? At the current time, the diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v index 886533586f..87b7a9a3be 100644 --- a/theories/Init/Tauto.v +++ b/theories/Init/Tauto.v @@ -27,7 +27,7 @@ Local Ltac simplif flags := | id: ?X1 |- _ => is_disj flags X1; elim id; intro; clear id | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ => (* generalize (id0 id1); intro; clear id0 does not work - (see Marco Maggiesi's bug PR#301) + (see Marco Maggiesi's BZ#301) so we instead use Assert and exact. *) assert X2; [exact (id0 id1) | clear id0] | id: forall (_ : ?X1), ?X2|- _ => |