aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2015-07-09Kernel: primitive projections handling of let-insMatthieu Sozeau
Fixes bug #4176 (actually two bugs in one) Correct computation of the type of primitive projections in presence of let-ins.
2015-07-06Merge branch 'v8.5' into trunkMaxime Dénès
2015-07-06Temporarily disable test file for #3922.Maxime Dénès
2015-07-06Test case for #4203, fixed by commit a51cce36.Maxime Dénès
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-07-01Notation: 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-29Fix test file for #4214 which was fixed by Hugo.Maxime Dénès
2015-06-29Better test case by PMP for #3948.Maxime Dénès
2015-06-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-26Fix bug #4254 with the help of J.H. JourdanMatthieu 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-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-11Add test-suite file for bug #3446.Matthieu Sozeau
2015-06-02Adding a test for bug #4057.Pierre-Marie Pédrot
2015-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-19Test for bug #4116.Pierre-Marie Pédrot
2015-05-18Removing test for opened bugs that were already present in the closed ↵Pierre-Marie Pédrot
test-suite.
2015-05-18Tentative 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-18Removing option -no-native-compiler from test #3539 since this option is nowHugo Herbelin
negated into -native-compiler.
2015-05-15Removing option -no-native-compiler from test #3539 since this option is nowHugo Herbelin
negated into -native-compiler.
2015-05-15Merge v8.5 into trunkHugo 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-13Fixing 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-13Better fixing #4198 such that the term to match is looked for beforeHugo Herbelin
the predicate, thus respecting the visual left-to-right top-down order (see a45bd5981092). This fixes CFGV.
2015-05-12Test for bug #4234.Pierre-Marie Pédrot
2015-05-11Test for bug #4232.Pierre-Marie Pédrot
2015-05-09Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).Hugo Herbelin
2015-05-09Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forHugo Herbelin
preserving compatibility of subst after #4214 being solved.
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-01Fixing computation of implicit arguments by position in fixpoints (#4217).Hugo Herbelin
2015-05-01Giving to "subst" a more natural semantic (fixing #4214) by using allHugo 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-22Tactical `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-22Test for #4198 (appcontext in return clause of match).Hugo Herbelin
2015-04-21Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argumentHugo Herbelin
in the presence of let-ins).
2015-04-17Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of severalHugo Herbelin
libraries at once (see #4193).
2015-04-16Test for bug #4190.Pierre-Marie Pédrot
2015-04-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-10Test for bug #3199.Pierre-Marie Pédrot
2015-04-09Better test-suite files, removing reliance on admit.Matthieu Sozeau
2015-04-09Fix declarations of instances to perform restriction of universeMatthieu Sozeau
instances as definitions and lemmas do (fixes bug# 4121).
2015-04-09Add test-suite file for bug #4120.Matthieu Sozeau
2015-04-09Merge branch 'v8.5' into trunkPierre Letouzey
2015-04-06Test for bug #3815.Pierre-Marie Pédrot
2015-03-31Fixing test-suite.Pierre-Marie Pédrot
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-29Adding test for bug #4165.Pierre-Marie Pédrot
2015-03-24Updating test-suite (see previous commit).Hugo Herbelin
2015-03-24Fixing computation of non-recursively uniform arguments in theHugo Herbelin
presence of let-ins. This fixes #3491.
2015-03-13Merge branch 'v8.5' into trunkArnaud Spiwack
2015-03-11Fix regression in HoTT_coq_014.vEnrico Tassi
Admitted was not using the partial proof to infer discharged variables. Now it does. The fix makes no sense, but restore the old behavior.
2015-03-11Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 07:26:01 +0000