aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1Gravatar herbelin2004-08-24
* Expansion du prédicat du 'match' vis à vis de la dépendance en le terme fi...Gravatar herbelin2004-08-24
* Prise en compte expansion du prédicat du 'match' vis à vis de la dépendanc...Gravatar herbelin2004-08-24
* Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)Gravatar herbelin2004-08-24
* Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...Gravatar herbelin2004-08-24
* Calling setoid_rewrite on a term H whose type (eq x y) was not an applicationGravatar sacerdot2004-08-24
* majGravatar filliatr2004-08-23
* Précisions message d'erreurGravatar herbelin2004-08-23
* Interpretation et affichage corrects des notations LetTuple, affichage des no...Gravatar herbelin2004-08-23
* Pas de notation v7 si purement en v8Gravatar herbelin2004-08-23
* Correction bug #830 : les noms des implicites temporaires étaient inconnus a...Gravatar herbelin2004-08-23
* The previous test file was truncated. New commit to fix the previousGravatar sacerdot2004-08-23
* Amélioration message d'erreur objet de récursion de type non inductifGravatar herbelin2004-08-06
* Apply implicit types to local binders tooGravatar herbelin2004-08-06
* Header V8Gravatar herbelin2004-08-03
* Protection contre un indice d'evar égal à 0Gravatar herbelin2004-08-03
* Zbool déjà dans ZArith_baseGravatar herbelin2004-08-03
* Minimisation utilisation NNPPGravatar herbelin2004-08-03
* Déclaration d'obsolescenceGravatar herbelin2004-08-03
* TypoGravatar herbelin2004-08-03
* RefGravatar herbelin2004-08-03
* Bug indexation des Require ImportGravatar herbelin2004-08-03
* Commentaires coqdocGravatar herbelin2004-08-01
* Commentaires coqdocGravatar herbelin2004-08-01
* Protection erreur find_eq_data dans decompEqThen et uniformisation messages d...Gravatar herbelin2004-07-30
* MAJGravatar herbelin2004-07-30
* Unbind the macosx dmg after creation to be able to build it again safelyGravatar herbelin2004-07-30
* majGravatar filliatr2004-07-29
* majGravatar filliatr2004-07-29
* Distinction location ocaml 3.08 ou pas (suite)Gravatar herbelin2004-07-29
* MAJ cible patchGravatar herbelin2004-07-29
* Protection unlocGravatar herbelin2004-07-29
* Distinction location ocaml 3.08 ou pasGravatar herbelin2004-07-29
* Bug join_locGravatar herbelin2004-07-29
* majGravatar filliatr2004-07-28
* Bug tactique fixGravatar herbelin2004-07-28
* majGravatar filliatr2004-07-27
* Utilisation de la variable camlp4 OCAML_308 plutôt que d'en reconstruire un...Gravatar herbelin2004-07-27
* majGravatar filliatr2004-07-26
* majGravatar filliatr2004-07-25
* majGravatar filliatr2004-07-25
* Plus de pa_ifdef dans CAMLP4EXTENDFLAGSGravatar herbelin2004-07-24
* majGravatar filliatr2004-07-23
* Several tests for the bug-fixed and improved new version ofGravatar sacerdot2004-07-23
* Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:Gravatar sacerdot2004-07-23
* Since setoid_{replace,rewrite} now uses replace there is a circularityGravatar sacerdot2004-07-23
* Setoid_replace.setoid_replace last argument (that was supposed to be alwaysGravatar sacerdot2004-07-23
* Setoid_replace.setoid_replace: last argument (that was supposed to beGravatar sacerdot2004-07-23
* "Print Setoids" command added.Gravatar sacerdot2004-07-23
* "Show Setoids" command added.Gravatar sacerdot2004-07-23