aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* Exploitation du 'let rec' + présentationGravatar herbelin2006-03-05
* New files for subtacGravatar coq2006-03-05
* tactic haRVey pour appeler haRVey (contrib/dp)Gravatar filliatr2006-03-02
* Correction bug #842 (rename d'une hyp du contexte)Gravatar herbelin2006-03-01
* appel de ZenonGravatar filliatr2006-03-01
* *** empty log message ***Gravatar filliatr2006-02-28
* dp: sortie WhyGravatar filliatr2006-02-27
* Work on recursive definitionsGravatar coq2006-02-22
* Add vernacular file for subtacGravatar coq2006-02-22
* Julien:Gravatar bertot2006-02-22
* Work with binder lists, problem of tyconsGravatar coq2006-02-21
* Latest fixes, should work fine now for non recursive definitions, although st...Gravatar coq2006-02-21
* Fix minor bugGravatar coq2006-02-20
* Forgot a fileGravatar coq2006-02-20
* Monday work, working with coercions and implicit argsGravatar coq2006-02-20
* Forgot another file...Gravatar coq2006-02-20
* Forgot one fileGravatar coq2006-02-20
* Rewrite of the subtac tactic, needs some work on implicit arguments.Gravatar coq2006-02-20
* bug correctionGravatar bertot2006-02-17
* Julien:Gravatar bertot2006-02-17
* changed the decomposition of an induction schemeGravatar coq2006-02-17
* firstorder fails gracefullly when encountering untypable higher-order termsGravatar corbinea2006-02-13
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
* very minor bug correction and cleanningGravatar bertot2006-02-09
* securing intros (we now use h_intro)Gravatar bertot2006-02-09
* Minor bugs fixesGravatar bertot2006-02-09
* Changing Set to Type for iter.Gravatar bertot2006-02-08
* One can use a measure {mes f x} instead of a well-founded relation in GenFixp...Gravatar bertot2006-02-08
* Julien:Gravatar bertot2006-02-08
* added mli 's for the nex functional induction (forgotten last time).Gravatar coq2006-02-03
* + Adding an error message when the function cannot be definedGravatar bertot2006-02-03
* protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)Gravatar barras2006-02-01
* protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)Gravatar barras2006-02-01
* New version of functional induction / inversion. By Julien Forest,Gravatar coq2006-02-01
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
* Suppression code pour hints nommés à la V7 (voire à la V6...)Gravatar herbelin2006-01-28
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...Gravatar herbelin2006-01-21
* Recursive Definition now supports functions with more than one argument.Gravatar coq2006-01-18
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser CoqGravatar herbelin2006-01-16
* - Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesGravatar herbelin2006-01-16
* Changing well founded induction to fix on accessibility proof in orderGravatar bertot2006-01-12
* remove warnings that were left in the directory contrib/interfaceGravatar bertot2006-01-11
* removes several warnings in contrib/interfaceGravatar bertot2006-01-11
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...Gravatar herbelin2005-12-30
* Nettoyage coqlibGravatar herbelin2005-12-30
* La distribution de Rocq/GRAPHS se fait via le serveur de contributions utilis...Gravatar herbelin2005-12-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-27 00:41:12 +0000