aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2009-10-25Restore (and test) broken chaining of lemmas in "apply in" in presenceherbelin
2009-10-25Add support for remaining side-conditions in "apply in as".herbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-17Fixed a notation bug when extending binder_constr with empty levelsherbelin
2009-10-04Removal of trailing spaces.serpyc
2009-09-27Fixed a bug in the interaction between dEqThen and inject_at_positionsherbelin
2009-09-27Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.herbelin
2009-09-27Delay the choice of eliminator in destruct/induction until we know ifherbelin
2009-09-22Add the option to automatically introduce variables declared before themsozeau
2009-09-20Only one "in" clause in "destruct" even for a multiple "destruct".herbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-11Ensures that let-in's in arities of inductive types work well. Maybe notherbelin
2009-07-20Move some examples for groebner into a test-suite fileletouzey
2009-07-15- Granted wish #2138 (support for local binders in syntax of Record fields).herbelin
2009-07-08Reactivation of pattern unification of evars in apply unification, inherbelin
2009-06-06Fixing bug #2106 ("match" compilation with multi-dependent constructor).herbelin
2009-06-02Adding a regression test about Bauer's example on coq-club ofherbelin
2009-06-02Fix script file using the "Manual Implicit" flag.msozeau
2009-05-10- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itherbelin
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
2009-04-10Fix premature optimisation in dependent induction: even variable args needmsozeau
2009-04-08- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingherbelin
2009-03-29Avoid inadvertent declaration of "on" as a keyword. New syntax ismsozeau
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-03-19coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...barras
2009-03-16Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"herbelin
2009-03-04illegal tactic application was having Ltac interpreter loopbarras
2009-02-23Add support for dependent "destruct" over terms in dependent types.herbelin
2009-02-06From v8.2 to trunk:herbelin
2009-02-04Report r11631 from 8.2 and handle non-dependent goals better inmsozeau
2009-01-22Fixes in the documentation of [dependent induction] and test-suitemsozeau
2009-01-18Backporting from v8.2 to trunk:herbelin
2009-01-13- Standardized prefix use of "Local"/"Global" modifiers as decided inherbelin
2009-01-07Uniformisation of some error messages + added test on setoid rewrite.herbelin
2008-12-16Finish fix for the treatment of [inverse] in [setoid_rewrite], making amsozeau
2008-12-16Fix for syntax changes in test-suite scripts.msozeau
2008-12-09About "apply in":herbelin
2008-12-03improved simplbarras
2008-12-02Add new directory for pre-compilation of files needed for further tests.herbelin
2008-12-02fixed kernel bug (de Bruijn) + test-suitebarras
2008-11-27added tests for hyps reorderingbarras
2008-11-09- Correction erreur dans test output Notation.vherbelin
2008-11-07Slight change of the semantics of user-given casts: they don't reallymsozeau
2008-11-07Add some example uses of the new record features in Record.v:msozeau
2008-11-07Fix a bug in the specialization by unification tactic related to the problemsmsozeau
2008-11-04Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)herbelin
2008-10-26Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiherbelin
2008-10-23Generalized implementation of generalization.msozeau
2008-10-19Retour en arrière pour raison de compatibilité sur la suppression du nf_evar herbelin
2008-10-18- Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-12 14:51:30 +0000