| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-07-27 | Fixing bug #3736 (anomaly instead of error/warning/silence on | Hugo Herbelin | |
| decidability scheme). Not clear to me why it is not a warning (in verbose mode) rather than silence when a scheme supposed to be built automatically cannot be built, as in: Set Decidable Equality Schemes. Inductive a := A with b := B. which could explain why a_beq and a_eq_dec as well as b_beq and b_eq_dec are not built. | |||
| 2015-07-22 | test-suite: add test for bug# 3743. | Matthieu Sozeau | |
| 2015-07-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-16 | Refining 71def2f8 on too strong occur-check limiting evar-evar | Hugo Herbelin | |
| unification in tactics. The relaxing of occur-check was ok but was leading trivial problems of the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into ?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems was not any more able to deal with. Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way, so that it behaves as if the occur-check had not been restricted. | |||
| 2015-07-16 | Remove old test file for #3819 (now fixed). | Maxime Dénès | |
| 2015-07-16 | Fixing bug #4240 (closure_of_filter was not ensuring refinement of | Hugo Herbelin | |
| former filter after 48509b61 and 3cd718c, because filtered let-ins were not any longer preserved). | |||
| 2015-07-16 | Test file for #3819. | Maxime Dénès | |
| 2015-07-09 | Kernel/Checker: Cleanup fixes of substitutions due to let-ins. | Matthieu Sozeau | |
| Avoid undeeded large substitutions, and add test-suite file for fixed bug 4283 in closed/ | |||
| 2015-07-09 | Kernel: primitive projections handling of let-ins | Matthieu Sozeau | |
| Fixes bug #4176 (actually two bugs in one) Correct computation of the type of primitive projections in presence of let-ins. | |||
| 2015-07-06 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-07-06 | Temporarily disable test file for #3922. | Maxime Dénès | |
| 2015-07-06 | Test case for #4203, fixed by commit a51cce36. | Maxime Dénès | |
| 2015-07-02 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-07-01 | Notation: use same level for "@" in constr: and pattern: (Close: #4272) | Enrico Tassi | |
| A possible script breakage can occur if one has a notation at level 11 that is also right associative (now 11 is left associative). Thanks Georges for debugging that. | |||
| 2015-06-29 | Fix test file for #4214 which was fixed by Hugo. | Maxime Dénès | |
| 2015-06-29 | Better test case by PMP for #3948. | Maxime Dénès | |
| 2015-06-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-06-26 | Fix bug #4254 with the help of J.H. Jourdan | Matthieu Sozeau | |
| 1) We now _assign_ the smallest possible arities to mutual inductive types and eventually add leq constraints on the user given arities. Remove useless limitation on instantiating algebraic universe variables with their least upper bound if they have upper constraints as well. 2) Do not remove non-recursive variables when computing minimal levels of inductives. 3) Avoid modifying user-given arities if not necessary to compute the minimal level of an inductive. 4) We correctly solve the recursive equations taking into account the user-declared level. | |||
| 2015-06-22 | Merge remote-tracking branch 'forge/v8.5' | Pierre Boutillier | |
| 2015-06-11 | Add test-suite file for bug #3446. | Matthieu Sozeau | |
| 2015-06-02 | Adding a test for bug #4057. | Pierre-Marie Pédrot | |
| 2015-06-01 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-05-19 | Test for bug #4116. | Pierre-Marie Pédrot | |
| 2015-05-18 | Removing test for opened bugs that were already present in the closed ↵ | Pierre-Marie Pédrot | |
| test-suite. | |||
| 2015-05-18 | Tentative fix for #3461: Anomaly: Uncaught exception ↵ | Pierre-Marie Pédrot | |
| Pretype_errors.PretypeError. Instad of trying to print the exception, we raise it in the tactic monad. | |||
| 2015-05-18 | Removing option -no-native-compiler from test #3539 since this option is now | Hugo Herbelin | |
| negated into -native-compiler. | |||
| 2015-05-15 | Removing option -no-native-compiler from test #3539 since this option is now | Hugo Herbelin | |
| negated into -native-compiler. | |||
| 2015-05-15 | Merge v8.5 into trunk | Hugo Herbelin | |
| Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API) | |||
| 2015-05-14 | #3953 now closed. | Hugo Herbelin | |
| 2015-05-13 | Fixing bug #4216: | Pierre-Marie Pédrot | |
| Internal error: Anomaly: Uncaught exception Not_found. Please report. An evarmap was lost because of an unsound typing primitive. | |||
| 2015-05-13 | Better fixing #4198 such that the term to match is looked for before | Hugo Herbelin | |
| the predicate, thus respecting the visual left-to-right top-down order (see a45bd5981092). This fixes CFGV. | |||
| 2015-05-12 | Test for bug #4234. | Pierre-Marie Pédrot | |
| 2015-05-11 | Test for bug #4232. | Pierre-Marie Pédrot | |
| 2015-05-09 | Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default). | Hugo Herbelin | |
| 2015-05-09 | Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for | Hugo Herbelin | |
| preserving compatibility of subst after #4214 being solved. | |||
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-05-01 | Fixing computation of implicit arguments by position in fixpoints (#4217). | Hugo Herbelin | |
| 2015-05-01 | Giving to "subst" a more natural semantic (fixing #4214) by using all | Hugo Herbelin | |
| equalities in configurations like x=y x=z === P(x,y,z) where it now produces === P(z,z,z) In particular (equations are processed from most ancient to most recent). Thanks to this, a "repeat subst" can just be a "subst" in List.v. Incidentally: moved a nf_enter to enter in subst_one, since the latter is normally called from other tactics having normalized evars. | |||
| 2015-04-22 | Tactical `progress` compares term up to potentially equalisable universes. | Arnaud Spiwack | |
| Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593. As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation. | |||
| 2015-04-22 | Test for #4198 (appcontext in return clause of match). | Hugo Herbelin | |
| 2015-04-21 | Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argument | Hugo Herbelin | |
| in the presence of let-ins). | |||
| 2015-04-17 | Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several | Hugo Herbelin | |
| libraries at once (see #4193). | |||
| 2015-04-16 | Test for bug #4190. | Pierre-Marie Pédrot | |
| 2015-04-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-04-10 | Test for bug #3199. | Pierre-Marie Pédrot | |
| 2015-04-09 | Better test-suite files, removing reliance on admit. | Matthieu Sozeau | |
| 2015-04-09 | Fix declarations of instances to perform restriction of universe | Matthieu Sozeau | |
| instances as definitions and lemmas do (fixes bug# 4121). | |||
| 2015-04-09 | Add test-suite file for bug #4120. | Matthieu Sozeau | |
| 2015-04-09 | Merge branch 'v8.5' into trunk | Pierre Letouzey | |
| 2015-04-06 | Test for bug #3815. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |