aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2011-12-16Fixing amazing loop when using eta-expansion in pattern-matching forherbelin
2011-12-12Proof using ...gareuselesinge
2011-12-07Fixing grammar resetting bug in the presence of levels initially emptyherbelin
2011-12-07Adapting test Existentials to new numbering strategy of evars (r14764).herbelin
2011-12-07Fixing a bug of commit r13310 (activating coercions only when moduleherbelin
2011-12-06Minor fixes to Argumentsgareuselesinge
2011-12-04A small test for type inference (used to be a regression at some time).herbelin
2011-12-04Fixing superflous newline in output of About when no parameter is renamed.herbelin
2011-12-04Discarding let-ins from the instances of the evars in theherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:28:54 +0000