aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2006-02-21Work with binder lists, problem of tyconscoq
2006-02-21Latest fixes, should work fine now for non recursive definitions, although st...coq
2006-02-20majcoq
2006-02-20Fix minor bugcoq
2006-02-20Forgot a filecoq
2006-02-20Monday work, working with coercions and implicit argscoq
2006-02-20Forgot another file...coq
2006-02-20Forgot one filecoq
2006-02-20Change in subtac modulescoq
2006-02-20Rewrite of the subtac tactic, needs some work on implicit arguments.coq
2006-02-19majcoq
2006-02-18majcoq
2006-02-17majcoq
2006-02-17bug correctionbertot
2006-02-17Julien:bertot
2006-02-17cleaningcoq
2006-02-17bug correction in the decomposition of an induction scheme.coq
2006-02-17changed the decomposition of an induction schemecoq
2006-02-16majcoq
2006-02-16added isProd to term.mli.coq
2006-02-15majcoq
2006-02-15continuing the generalization of "induction". Now induction schemescoq
2006-02-14majcoq
2006-02-13majcoq
2006-02-13Bug correction in saving proofs: If a hook opens a proof but does not close i...bertot
2006-02-13firstorder fails gracefullly when encountering untypable higher-order termscorbinea
2006-02-12majcoq
2006-02-12Bug Scopeherbelin
2006-02-12Zmax et Zminmaxherbelin
2006-02-12Nettoyage Zmin.v, création Zmax.v et Zminmax.vherbelin
2006-02-12Nettoyage Bool:herbelin
2006-02-12Unification max_case et max_case2herbelin
2006-02-12Unification min_case et min_case2herbelin
2006-02-11majcoq
2006-02-11Commentaires et compatibilité coqdocherbelin
2006-02-10majcoq
2006-02-10induction now admits multiple induction arguments. The principle mustcoq
2006-02-10code mortherbelin
2006-02-09majcoq
2006-02-09very minor bug correction and cleanningbertot
2006-02-09securing intros (we now use h_intro)bertot
2006-02-09Minor bugs fixesbertot
2006-02-08majcoq
2006-02-08Changing Set to Type for iter.bertot
2006-02-08One can use a measure {mes f x} instead of a well-founded relation in GenFixp...bertot
2006-02-08Julien:bertot
2006-02-08Localisation des erreurs de sorte du prétypageherbelin
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
2006-02-07majcoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 14:41:51 +0000