| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-23 | Recognizing Z in romega up to conversion. | Hugo Herbelin | |
| 2017-11-23 | Using is_conv rather than eq_constr to find `nat` or `Z` in omega. | Hugo Herbelin | |
| Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717. | |||
| 2017-11-23 | Fixing a 8.7 regression of ring_simplify in ArithRing. | Hugo Herbelin | |
| With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191). | |||
| 2017-11-23 | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Maxime Dénès | |
| 2017-11-22 | Fix universe polymorphic Program obligations. | Matthieu Sozeau | |
| The universes of the obligations should all be non-algebraic as they might appear in instances of other obligations and instances only take non-algebraic universes as arguments. | |||
| 2017-11-20 | Merge PR #6166: Fix regression in treating Defined as defined | Maxime Dénès | |
| 2017-11-20 | Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵ | Maxime Dénès | |
| (clause "where" with implicit arguments) | |||
| 2017-11-20 | Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵ | Maxime Dénès | |
| unbound rel | |||
| 2017-11-19 | Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Gaëtan Gilbert | |
| 2017-11-15 | Fix regression in treating Defined as defined | Tej Chajed | |
| Fixes #6165. | |||
| 2017-11-15 | Fix #5761: cbv on undefined evars under binders produces unbound rel | Gaëtan Gilbert | |
| When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case. | |||
| 2017-11-14 | Fixes #6129 (declaration of coercions made compatible with local definitions). | Hugo Herbelin | |
| 2017-11-14 | One more step in fixing #5762 ("where" clause). | Hugo Herbelin | |
| We improve one step further the heuristics to sort out if a variable is a notation variable or a named variable. This allows to support the following which was still failing. Reserved Notation "# x" (at level 0). Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I). We rely here on the property that a binding variable of same name as a notation variables is itself considered bound by the notation. This becomes however to be a bit tricky for sorting out if the variable has to be output to the glob file or not. | |||
| 2017-11-13 | Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac. | Maxime Dénès | |
| 2017-11-06 | Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to ↵ | Maxime Dénès | |
| alphabet). | |||
| 2017-11-06 | Merge PR #1139: Add a linter. | Maxime Dénès | |
| 2017-11-05 | Refining PR#924 (insensitivity of projection heuristics to alphabet). | Hugo Herbelin | |
| We refine the criterion for selecting a projection. Before PR#924 it was alphabetic (i.e. morally "random" up to alpha-conversion). After PR#924 it was chronological. We refine a bit more by giving priority to simple projections when they exist over projections which include an evar instantiation (and which may actually be ill-typed). | |||
| 2017-11-04 | Adding support for syntax "let _ := e in e'" in Ltac. | Hugo Herbelin | |
| Adding a file fixing #5996 and which uses this feature. | |||
| 2017-11-03 | Merge PR #6047: A generic printer for ltac values | Maxime Dénès | |
| 2017-11-03 | Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵ | Maxime Dénès | |
| variables). | |||
| 2017-11-03 | Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition). | Maxime Dénès | |
| 2017-11-02 | Binding ltac printing functions to the system of generic printing. | Hugo Herbelin | |
| This concerns pr_value and message_of_value. This has a few consequences. For instance, no more ad hoc message "a term" or "a tactic", when not enough information is available for printing, one gets a generic message "a value of type foobar". But we also have more printers, satisfying e.g. request #5786. | |||
| 2017-10-30 | Fixing #2881 ("change with" failing in an Ltac definition). | Hugo Herbelin | |
| We fix by interpreting the pattern in "change pat with term" in strict mode by using the same interning code as for "match goal" (even if the pattern is dropped afterwards). | |||
| 2017-10-28 | Fixing #5401 (printing of patterns with bound anonymous variables). | Hugo Herbelin | |
| This fixes also #5731, #6035, #5364. | |||
| 2017-10-27 | Merge PR #677: Trunk+abstracting injection flags | Maxime Dénès | |
| 2017-10-26 | Passing around the flag for injection so that tactics calling inj at | Hugo Herbelin | |
| ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281. | |||
| 2017-10-25 | Put newlines at the end of files. | Gaëtan Gilbert | |
| 2017-10-23 | Move bug files to match their new GitHub ID (fixes #6001). | Théo Zimmermann | |
| 2017-10-20 | Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" ↵ | Maxime Dénès | |
| clause of an inductive definitions | |||
| 2017-10-17 | Adding a test for bug BZ#5692. | Pierre-Marie Pédrot | |
| 2017-10-15 | [stdlib] Fix warnings on deprecated `Add Setoid` | Emilio Jesus Gallego Arias | |
| The test suite cases are preserved until the feature is actually removed. | |||
| 2017-10-10 | Merge PR #768: Omega and romega know about context definitions (fix old bug 148) | Maxime Dénès | |
| 2017-10-06 | Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵ | Maxime Dénès | |
| "_something") | |||
| 2017-10-06 | Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ↵ | Maxime Dénès | |
| inductive definition) | |||
| 2017-10-06 | Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly ↵ | Maxime Dénès | |
| BZ#4852) | |||
| 2017-10-05 | Omega now aware of context variables with bodies (in type Z or nat) (fix bug ↵ | Pierre Letouzey | |
| 148) For compatibility, this extra feature of omega could be disabled via Unset Omega UseLocalDefs. Caveat : for now, real let-ins inside goals or hyps aren't handled, use some "cbv zeta" reduction if you want to get rid of them. And context definitions whose types aren't Z or nat are ignored, some manual "unfold" are still mandatory if expanding these definitions will help omega. | |||
| 2017-10-05 | Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵ | Maxime Dénès | |
| BZ#5757) | |||
| 2017-10-05 | Extraction: reduce eta-redexes whose cores are atomic (solves indirectly ↵ | Pierre Letouzey | |
| BZ#4852) This code simplification isn't that important, but it can trigger further simplifications elsewhere, see for instance BZ#4852. NB: normally, the extraction favors eta-expanded forms, since that's the usual way to avoid issues about '_a type variables that cannot be generalized. But the atomic eta-reductions done here shouldn't be problematic (no applications put outside of functions). | |||
| 2017-10-05 | Fixing BZ#5769 (variable of type "_something" was named after invalid "_"). | Hugo Herbelin | |
| 2017-10-05 | Fixing #5765 (an anomaly with 'pat in parameters of inductive definition). | Hugo Herbelin | |
| 2017-10-05 | Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.). | Hugo Herbelin | |
| This allows e.g. the following to work: Reserved Notation "* a" (at level 70). Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m). We seize this opportunity to make main calls to Metasyntax to depend on an arbitrary env rather than on Global.env. Incidentally, this fixes a little coqdoc bug in classifying the inductive type referred to in the "where" clause. | |||
| 2017-10-04 | Merge PR #1006: fix: ssrmatching and primitive projections | Maxime Dénès | |
| 2017-10-04 | Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial). | Maxime Dénès | |
| 2017-09-27 | Moving setting of "cleared" evar flag directly in Evd.restrict. | Hugo Herbelin | |
| In particular, this fixes #5757 which used restrict_evar to refine the information on the source of an evar, and which should have set the "cleared" flag. Also renaming flag "restricted" since it is not only about "clear". I guess this is what we want in general, but I did not survey all uses of restrict_evar so, maybe, this should be refined further. | |||
| 2017-09-25 | Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ↵ | Maxime Dénès | |
| inductive types) | |||
| 2017-09-25 | Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵ | Maxime Dénès | |
| 4e70791). | |||
| 2017-09-23 | Fixing #5755 (discharging of inductive types not correct with let-ins). | Hugo Herbelin | |
| The number of effective parameters was used where the number of declarations in the signature of parameters should have been used. | |||
| 2017-09-23 | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791). | Hugo Herbelin | |
| 2017-09-21 | A possible fix to BZ#5750 (ability to print context of ltac subterm match). | Hugo Herbelin | |
| The main fix is to use is_ident_soft. The rest of the commit is to provide something a bit more appealing than "?M-1". | |||
| 2017-09-20 | ssr: fix canonical strucut key comparison with primproj on | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |