aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
* Adding "New Functional Scheme" Gravatar jforest2006-03-20
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* Cleaning dead code Gravatar jforest2006-03-16
* + Debugging and cleaning functional principle generation tacticGravatar jforest2006-03-14
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* -Debugging multiple induction, a bug appeared when having functionGravatar courtieu2006-03-12
* cleaning Gravatar jforest2006-03-10
* Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain is_emp...Gravatar jforest2006-03-07
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 04:52:53 +0000