aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2005-11-14adds the the case VernacShow(ShowMatch _) in the pattern-matching construct,bertot
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-11-07Adds tools to help in defining new general recursive functionsbertot
2005-11-02Types inductifs parametriquesmohring
2005-09-16changed the syntax categories of arguments of functional schemecoq
2005-08-19pas besoin de List.length pour savoir si une liste est videletouzey
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
2005-08-18code cleaning. No changes as far as tested.coq
2005-08-17new congruencecorbinea
2005-07-15Subtac: traitement correct des existentielles et de la récursion.coq
2005-07-15reflexive tautocorbinea
2005-07-13General recursive definitions on well founded orders supportcoq
2005-06-24Dp: ajout d'abstraction aux applications de fonction non premier ordrecoq
2005-06-24dp: ajout des prédicats de sortescoq
2005-06-15Dp : ajoût des existentielscoq
2005-06-09dp: traitement des fixpointscoq
2005-06-08traitement des casecoq
2005-05-26Correction of a bug in functional scheme. It raised with mutualcoq
2005-05-26Add a guard for V7 mode, CVS compiles cleanly again :)coq
2005-05-25Added subtac contrib.coq
2005-05-24dp: ajout du prouveur Zenoncoq
2005-05-20New command: "Print Ltac qualid" to print user defined tactics.sacerdot
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-05-19added VernacBacktrack (new backtracking command dedicated tocoq
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-05-15Allow auto to have a parametric argument (wish #967)herbelin
2005-05-03Open Scope non Local malencontreuxherbelin
2005-05-02Utilisation Z_scopeherbelin
2005-04-21Gestion du forall et envoie d'axiome à la procédurecoq
2005-04-07dp: traitement des definitionscoq
2005-04-05Problemes de renommage reglescoq
2005-03-24symboles de fonctions globaux traitescoq
2005-03-22Ajout de l'axiome du but prouve par la tactique simplificoq
2005-03-18appel de Simplify depuis Coqcoq
2005-03-16tactiques prouveurs premier ordre dans contrib/dp/coq
2005-03-16nouvelles tactiques pour appeler des procedures de decision du premier ordrecoq
2005-03-15Unsharing before exportation to ensure uniqueness of xml id'sherbelin
2005-03-07Added 'clear - id' to clear all hypotheses except the ones dependent in the s...herbelin
2005-02-21Pas de dépendance en Omegaherbelin
2005-02-21Correction de bugs: coq_false et coq_true au lieu de coq_False et coq_trueherbelin
2005-02-21- changement ordre arguments interp_goal_concl pour permettre applicationherbelin
2005-02-21- Correction de bugsherbelin
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
2005-02-18Standardisation of function names about structuresherbelin
2005-02-18Standardisation of function names about global references (especially, renami...herbelin
2005-02-18Déboggueur et code mortherbelin
2005-02-17Correction bug #922 (problème dans depend) + formattage débogueurherbelin
2005-02-12Uniformisation de destApplication en destAppherbelin
2005-02-12Ajout Print Canonical Structuresherbelin
2005-02-06Nettoyage et documentation de Libraryherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 16:10:48 +0000