aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2011-11-30Quick hack to avoid anomaly on using Program w/o having required JMeq.herbelin
2011-11-28Extraction: Richer patterns in matchs as proposed by P.N. Tollitteletouzey
2011-11-26Fixed a bug in postprocessing dependencies in pattern-matching compilationherbelin
2011-11-21Renamig support added to "Arguments"gareuselesinge
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-11-21New Arguments vernaculargareuselesinge
2011-11-21Configurable simpl tacticgareuselesinge
2011-11-21Extend the computation of dependencies in pattern-matching compilationherbelin
2011-11-21Optimizing the compilation of unused aliases in pattern-matching.herbelin
2011-11-21Fixing postprocessing bugs in pattern-matching compilation.herbelin
2011-11-21Changed the way to detect if an "as" patterns is expanded or not. Theherbelin
2011-11-21Updating Cases.v test.herbelin
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-17Fixing new bug introduced in r14665 when fixing bug #1834.herbelin
2011-11-16Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).herbelin
2011-11-16Suppression fichier Case8.v redondantherbelin
2011-11-08Improved check is_open_canonical_projectiongareuselesinge
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
2011-11-06Fixing incorrect change to pattern-unification over Meta's introducedherbelin
2011-11-06Fixing tactic remember not correctly checking preservation of typingherbelin
2011-10-25Regression tests for bugs #2613 and #2616.herbelin
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2011-10-25Fixing "destruct" test.herbelin
2011-10-25New strategy to infer return predicate of match construct whenherbelin
2011-10-24Mod_subst: Attempt to fix #2608letouzey
2011-10-24Fixing another bug revealing ill-typed use of evar restriction.herbelin
2011-10-22Use full conversion for checking type of holes in destruct over aherbelin
2011-10-18Fix bug #2473 due to wrong folding of the evar environmentmsozeau
2011-10-18Fix inductive coercion code in Program (bug #2378)msozeau
2011-10-18Fix bug #2586 and enhance clsubst* as well as a side effectmsozeau
2011-10-17Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...msozeau
2011-10-12test-suite: non-regression test for bug #2603letouzey
2011-10-11Added test for bug #2615herbelin
2011-10-11Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedherbelin
2011-10-07fsetdec : non-atomic elements are now transformed as variables first (fix #2464)letouzey
2011-10-07Improved handling of element equalities in fsetdec (fix #2467)letouzey
2011-10-05Fixing critical inductive polymorphism bug found by Bruno.herbelin
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-22test-suite : an additional message displayed by Notation2.vletouzey
2011-09-22Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.letouzey
2011-09-19Fix test-suite/ide for repository compiled without -local (fix #2600)letouzey
2011-09-17Various fixes in the Makefilesletouzey
2011-09-15Omega aware of Z.pred (fix #1912)letouzey
2011-09-15Re-allowing assumptions during proofs seems safe now (fix #2411)letouzey
2011-09-06test-suite/ide: misc improvementletouzey
2011-09-05fake_ide: a short program to mimic an ide talking to coqtop -ideslaveletouzey
2011-08-10Fixing printing bug with last trailing non-maximally implicitherbelin
2011-08-10Partly revert commit r14389 about relaxing the condition for being a keywordherbelin
2011-08-08Be a bit less aggressive in declaring idents as keywords in notationsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 14:59:43 +0000