aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Fixing bug #2634 (unscoped notations were disturbing theGravatar herbelin2011-12-18
* Fixed a Not_found bug when declaring in a section some implicitGravatar herbelin2011-12-18
* Added ability to take the type of applied metas into account whenGravatar herbelin2011-12-17
* Command Arguments: standardizing format of error messages and American spelling.Gravatar herbelin2011-12-17
* Bypassing the use of (currently unimplemented) "Show Script" in testsGravatar herbelin2011-12-17
* Fixing format of complexity bug Notations.v.Gravatar herbelin2011-12-17
* Fixing amazing loop when using eta-expansion in pattern-matching forGravatar herbelin2011-12-16
* Proof using ...Gravatar gareuselesinge2011-12-12
* Fixing grammar resetting bug in the presence of levels initially emptyGravatar herbelin2011-12-07
* Adapting test Existentials to new numbering strategy of evars (r14764).Gravatar herbelin2011-12-07
* Fixing a bug of commit r13310 (activating coercions only when moduleGravatar herbelin2011-12-07
* Minor fixes to ArgumentsGravatar gareuselesinge2011-12-06
* A small test for type inference (used to be a regression at some time).Gravatar herbelin2011-12-04
* Fixing superflous newline in output of About when no parameter is renamed.Gravatar herbelin2011-12-04
* Discarding let-ins from the instances of the evars in theGravatar herbelin2011-12-04
* Quick hack to avoid anomaly on using Program w/o having required JMeq.Gravatar herbelin2011-11-30
* Extraction: Richer patterns in matchs as proposed by P.N. TollitteGravatar letouzey2011-11-28
* Fixed a bug in postprocessing dependencies in pattern-matching compilationGravatar herbelin2011-11-26
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* New Arguments vernacularGravatar gareuselesinge2011-11-21
* Configurable simpl tacticGravatar gareuselesinge2011-11-21
* Extend the computation of dependencies in pattern-matching compilationGravatar herbelin2011-11-21
* Optimizing the compilation of unused aliases in pattern-matching.Gravatar herbelin2011-11-21
* Fixing postprocessing bugs in pattern-matching compilation.Gravatar herbelin2011-11-21
* Changed the way to detect if an "as" patterns is expanded or not. TheGravatar herbelin2011-11-21
* Updating Cases.v test.Gravatar herbelin2011-11-21
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* Fixing new bug introduced in r14665 when fixing bug #1834.Gravatar herbelin2011-11-17
* Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).Gravatar herbelin2011-11-16
* Suppression fichier Case8.v redondantGravatar herbelin2011-11-16
* Improved check is_open_canonical_projectionGravatar gareuselesinge2011-11-08
* Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsGravatar letouzey2011-11-07
* Fixing incorrect change to pattern-unification over Meta's introducedGravatar herbelin2011-11-06
* Fixing tactic remember not correctly checking preservation of typingGravatar herbelin2011-11-06
* Regression tests for bugs #2613 and #2616.Gravatar herbelin2011-10-25
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* Fixing "destruct" test.Gravatar herbelin2011-10-25
* New strategy to infer return predicate of match construct whenGravatar herbelin2011-10-25
* Mod_subst: Attempt to fix #2608Gravatar letouzey2011-10-24
* Fixing another bug revealing ill-typed use of evar restriction.Gravatar herbelin2011-10-24
* Use full conversion for checking type of holes in destruct over aGravatar herbelin2011-10-22
* Fix bug #2473 due to wrong folding of the evar environmentGravatar msozeau2011-10-18
* Fix inductive coercion code in Program (bug #2378)Gravatar msozeau2011-10-18
* Fix bug #2586 and enhance clsubst* as well as a side effectGravatar msozeau2011-10-18
* Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...Gravatar msozeau2011-10-17
* test-suite: non-regression test for bug #2603Gravatar letouzey2011-10-12
* Added test for bug #2615Gravatar herbelin2011-10-11
* Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedGravatar herbelin2011-10-11
* fsetdec : non-atomic elements are now transformed as variables first (fix #2464)Gravatar letouzey2011-10-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 19:51:39 +0000