aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
* add names of theorems in outputGravatar jnarboux2011-06-18
* Tests de nsatz avec la geometrieGravatar pottier2011-06-16
* Added full pattern-unification on Meta for tactic unification.Gravatar herbelin2011-06-13
* Another bug of Scheme Induction (generated names dep/nodep were swapped).Gravatar herbelin2011-06-13
* Fixing an anomaly in Scheme Induction.Gravatar herbelin2011-06-13
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
* Fixing another bug with "_" intro pattern.Gravatar herbelin2011-06-10
* Made use of "_" in repeated use of intros_patterns work (withGravatar herbelin2011-06-10
* ring2, cring, nsatz avec type classe avec parametres plus notationsGravatar pottier2011-06-10
* Mini-test for etaGravatar herbelin2011-05-26
* Partial fix for accepting bound variables with same name as implicitGravatar herbelin2011-05-26
* Fixing discriminate for identity.Gravatar herbelin2011-05-26
* Add simple test of bullet behaviour.Gravatar aspiwack2011-05-17
* Fixes in the test-suite after modularisation of ZArith and coGravatar letouzey2011-05-06
* Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixedGravatar herbelin2011-04-28
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vGravatar herbelin2011-04-08
* Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)Gravatar letouzey2011-03-16
* Fix inductive_template building ill-typed evars, and update test-suite scriptsGravatar msozeau2011-03-13
* Improved define_evar_as_lambda which was creating an unrelated new evarGravatar herbelin2011-03-05
* Try to fix the behavior of clenv_missing used when declaring hintsGravatar letouzey2011-02-22
* Some fixes of the test-suite scriptsGravatar letouzey2011-02-21
* Fix test-suite script.Gravatar msozeau2011-02-21
* Correct handling of existential variables when multiple differentGravatar msozeau2011-02-08
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* Fixing an uncaught exception bug with use of vmcastGravatar herbelin2011-01-07
* Remove the two-argument variant of "decide equality"Gravatar glondu2010-12-23
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
* Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).Gravatar herbelin2010-12-04
* Fixing bug using explictly declared implicit arguments in inductive arities.Gravatar herbelin2010-12-03
* Fixing a bug introduced in r12304 (move of interpretation ofGravatar herbelin2010-12-02
* SearchAbout: who has never been annoyed by the [ ] syntax ?Gravatar letouzey2010-11-19
* An experimental support for open constrs in hints and in "using"Gravatar herbelin2010-10-31
* test-suite: fix success/unification.vGravatar glondu2010-10-07
* test-suite: fix success/Typeclasses.vGravatar glondu2010-10-05
* test-suite: fix success/AdvancedCanonicalStructure.vGravatar glondu2010-10-05
* Export definition of type implicits_list for contribs + fixed aGravatar herbelin2010-10-05
* Fixing bugs in previous commits about implicit arguments:Gravatar herbelin2010-10-04
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Improve handling of metas as evars in unification (patch by Hugo)Gravatar letouzey2010-09-30
* Fixed a problem introduced in r12607 after pattern_of_constr servedGravatar herbelin2010-09-17
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
* Improving a few error messages in Ltac interpretationGravatar herbelin2010-09-11
* unification des tactiques nsatz pour R Z avec celle des anneaux integresGravatar pottier2010-07-28
* nstaz pour les anneaux integres et les setoides, R Z et QGravatar pottier2010-07-27
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fix compilation and test-suite of nsatzGravatar glondu2010-07-12