aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* majGravatar coq2006-02-21
* 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
* majGravatar coq2006-02-20
* 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
* Change in subtac modulesGravatar coq2006-02-20
* Rewrite of the subtac tactic, needs some work on implicit arguments.Gravatar coq2006-02-20
* majGravatar coq2006-02-19
* majGravatar coq2006-02-18
* majGravatar coq2006-02-17
* bug correctionGravatar bertot2006-02-17
* Julien:Gravatar bertot2006-02-17
* cleaningGravatar coq2006-02-17
* bug correction in the decomposition of an induction scheme.Gravatar coq2006-02-17
* changed the decomposition of an induction schemeGravatar coq2006-02-17
* majGravatar coq2006-02-16
* added isProd to term.mli.Gravatar coq2006-02-16
* majGravatar coq2006-02-15
* continuing the generalization of "induction". Now induction schemesGravatar coq2006-02-15
* majGravatar coq2006-02-14
* majGravatar coq2006-02-13
* Bug correction in saving proofs: If a hook opens a proof but does not close i...Gravatar bertot2006-02-13
* firstorder fails gracefullly when encountering untypable higher-order termsGravatar corbinea2006-02-13
* majGravatar coq2006-02-12
* Bug ScopeGravatar herbelin2006-02-12
* Zmax et ZminmaxGravatar herbelin2006-02-12
* Nettoyage Zmin.v, création Zmax.v et Zminmax.vGravatar herbelin2006-02-12
* Nettoyage Bool:Gravatar herbelin2006-02-12
* Unification max_case et max_case2Gravatar herbelin2006-02-12
* Unification min_case et min_case2Gravatar herbelin2006-02-12
* majGravatar coq2006-02-11
* Commentaires et compatibilité coqdocGravatar herbelin2006-02-11
* majGravatar coq2006-02-10
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
* code mortGravatar herbelin2006-02-10
* majGravatar coq2006-02-09
* 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
* majGravatar coq2006-02-08
* 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
* Localisation des erreurs de sorte du prétypageGravatar herbelin2006-02-08
* Ajout bibliothèque String de Laurent ThéryGravatar herbelin2006-02-08
* Ajout bibliothèque String de Laurent ThéryGravatar herbelin2006-02-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 04:43:09 +0000