aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* Move some examples for groebner into a test-suite fileGravatar letouzey2009-07-20
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Fixing bug #2106 ("match" compilation with multi-dependent constructor).Gravatar herbelin2009-06-06
* Adding a regression test about Bauer's example on coq-club ofGravatar herbelin2009-06-02
* Fix script file using the "Manual Implicit" flag.Gravatar msozeau2009-06-02
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingGravatar herbelin2009-04-08
* Avoid inadvertent declaration of "on" as a keyword. New syntax isGravatar msozeau2009-03-29
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...Gravatar barras2009-03-19
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
* Add support for dependent "destruct" over terms in dependent types.Gravatar herbelin2009-02-23
* From v8.2 to trunk:Gravatar herbelin2009-02-06
* Report r11631 from 8.2 and handle non-dependent goals better inGravatar msozeau2009-02-04
* Fixes in the documentation of [dependent induction] and test-suiteGravatar msozeau2009-01-22
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13
* Uniformisation of some error messages + added test on setoid rewrite.Gravatar herbelin2009-01-07
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
* Fix for syntax changes in test-suite scripts.Gravatar msozeau2008-12-16
* About "apply in":Gravatar herbelin2008-12-09
* improved simplGravatar barras2008-12-03
* Add new directory for pre-compilation of files needed for further tests.Gravatar herbelin2008-12-02
* fixed kernel bug (de Bruijn) + test-suiteGravatar barras2008-12-02
* added tests for hyps reorderingGravatar barras2008-11-27
* - Correction erreur dans test output Notation.vGravatar herbelin2008-11-09
* Slight change of the semantics of user-given casts: they don't reallyGravatar msozeau2008-11-07
* Add some example uses of the new record features in Record.v:Gravatar msozeau2008-11-07
* Fix a bug in the specialization by unification tactic related to the problemsGravatar msozeau2008-11-07
* Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)Gravatar herbelin2008-11-04
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* Retour en arrière pour raison de compatibilité sur la suppression du nf_evar Gravatar herbelin2008-10-19
* - Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)Gravatar herbelin2008-10-18
* test-suite: more utf8 tests, a test of ! ? and so on in rewritesGravatar letouzey2008-10-14
* Minor fixes related to coqdoc and --interpolate and the dependentGravatar msozeau2008-10-03
* Report improvements in Equations to the dependent elimination tactic:Gravatar msozeau2008-09-15
* Finish debugging the unification machinery in [Equations]. Do the _compGravatar msozeau2008-09-13
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
* Fixes in dependent induction tactic, putting things in better order forGravatar msozeau2008-09-11
* Some more debugging of [Equations], unification still not perfect.Gravatar msozeau2008-09-11
* More debugging of [Equations], now able to discharge even the heavilyGravatar msozeau2008-09-07
* Correct handling of implicit arguments in [Equations] definitions,Gravatar msozeau2008-09-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 19:36:38 +0000