aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* majGravatar coq2006-02-07
* oubli de code de debuggingGravatar herbelin2006-02-07
* Messages nth brancheGravatar herbelin2006-02-07
* Idem numbering of 'Unfold', 'simpl', ...Gravatar herbelin2006-02-07
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
* Ajout pluralGravatar herbelin2006-02-07
* Mise en conformité de l'ordre des occurrences de pattern avec l'affichageGravatar herbelin2006-02-07
* MAJGravatar herbelin2006-02-07
* majGravatar coq2006-02-06
* Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru...Gravatar herbelin2006-02-06
* warning seulement si mode verboseGravatar herbelin2006-02-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 19:43:03 +0000