aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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
2008-10-14test-suite: more utf8 tests, a test of ! ? and so on in rewritesletouzey
2008-10-03Minor fixes related to coqdoc and --interpolate and the dependentmsozeau
2008-09-15Report improvements in Equations to the dependent elimination tactic:msozeau
2008-09-13Finish debugging the unification machinery in [Equations]. Do the _compmsozeau
2008-09-12Add a type argument to letin_tac instead of using casts and recomputingmsozeau
2008-09-11Fixes in dependent induction tactic, putting things in better order formsozeau
2008-09-11Some more debugging of [Equations], unification still not perfect.msozeau
2008-09-07More debugging of [Equations], now able to discharge even the heavilymsozeau
2008-09-03Correct handling of implicit arguments in [Equations] definitions,msozeau
2008-09-02Add support for recursive definitions to [Equations], deciding if amsozeau
2008-09-02Initial implementation of a new command to define (dependent) functions bymsozeau
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-08-05Correction de bugs:herbelin
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
2008-07-11Correction d'un autre bug autour de la gestion des niveaux vides deherbelin
2008-07-07Fix implicit arguments in sections bug and check for resolution of evars whenmsozeau
2008-06-29Préférence donnée aux constantes qui ne sont pas des projectionsherbelin
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
2008-06-10- Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-05-30Improve the dependent induction tactic to automatically find themsozeau
2008-05-26Résolution bug #1850 sur notations avec niveaux inconnus deherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 08:07:32 +0000