aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* majGravatar filliatr2004-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6044 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6043 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6042 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6041 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6040 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6039 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6038 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make ↵Gravatar herbelin2004-08-26
| | | | | | depend en erreur; déplacement de pa_ifdef dans MMakefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6037 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6036 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1Gravatar herbelin2004-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Expansion du prédicat du 'match' vis à vis de la dépendance en le terme ↵Gravatar herbelin2004-08-24
| | | | | | filtré (utilisation de Anonymous pour signaler une dépendance formelle, en relation avec le nommage dans Inductiveops.type_case_branches); uniformisation/nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte expansion du prédicat du 'match' vis à vis de la ↵Gravatar herbelin2004-08-24
| | | | | | dépendance en le terme filtré (cf Indrec) + déplacement routines pour Cases à la V7 dans Pretyping) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6031 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)Gravatar herbelin2004-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement des fonctions de typage des predicate de Cases a la V7 de ↵Gravatar herbelin2004-08-24
| | | | | | inductiveops vers pretyping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Calling setoid_rewrite on a term H whose type (eq x y) was not an applicationGravatar sacerdot2004-08-24
| | | | | | | | | | | | of a setoid equality was erroneously considered an assertion failure instead of an user error. Note: in this case the tactic should try the rewrite tactic. However, since rewrite recursively calls setoid_rewrite in this case, this solution can diverge. This will be fixed in a future commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6028 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Précisions message d'erreurGravatar herbelin2004-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Interpretation et affichage corrects des notations LetTuple, affichage des ↵Gravatar herbelin2004-08-23
| | | | | | notations If git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas de notation v7 si purement en v8Gravatar herbelin2004-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6023 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #830 : les noms des implicites temporaires étaient inconnus ↵Gravatar herbelin2004-08-23
| | | | | | au moment de l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6021 85f007b7-540e-0410-9357-904b9bb8a0f7
* The previous test file was truncated. New commit to fix the previousGravatar sacerdot2004-08-23
| | | | | | | commit error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration message d'erreur objet de récursion de type non inductifGravatar herbelin2004-08-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6019 85f007b7-540e-0410-9357-904b9bb8a0f7
* Apply implicit types to local binders tooGravatar herbelin2004-08-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6017 85f007b7-540e-0410-9357-904b9bb8a0f7
* Header V8Gravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre un indice d'evar égal à 0Gravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6015 85f007b7-540e-0410-9357-904b9bb8a0f7
* Zbool déjà dans ZArith_baseGravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minimisation utilisation NNPPGravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6012 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déclaration d'obsolescenceGravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6011 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6010 85f007b7-540e-0410-9357-904b9bb8a0f7
* RefGravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6009 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug indexation des Require ImportGravatar herbelin2004-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6006 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commentaires coqdocGravatar herbelin2004-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6004 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commentaires coqdocGravatar herbelin2004-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection erreur find_eq_data dans decompEqThen et uniformisation messages ↵Gravatar herbelin2004-07-30
| | | | | | d'erreur, et généralisation onNegatedEquality git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6000 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unbind the macosx dmg after creation to be able to build it again safelyGravatar herbelin2004-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5997 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5996 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Distinction location ocaml 3.08 ou pas (suite)Gravatar herbelin2004-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5993 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ cible patchGravatar herbelin2004-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection unlocGravatar herbelin2004-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5990 85f007b7-540e-0410-9357-904b9bb8a0f7
* Distinction location ocaml 3.08 ou pasGravatar herbelin2004-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug join_locGravatar herbelin2004-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5985 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug tactique fixGravatar herbelin2004-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5981 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5980 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de la variable camlp4 OCAML_308 plutôt que d'en reconstruire ↵Gravatar herbelin2004-07-27
| | | | | | une nous-mêmes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5979 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5978 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5977 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-23 03:42:49 +0000