aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-09-03V7 .v files for Setoid_* and Ring over setoids commented out.sacerdot
To re-enable them I would need to back-port theories/Setoids/Setoid.v from the new syntax to the old syntax. However, since the translator is going to be removed from the next major Coq version, I am not doing it (unless required to). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6046 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6045 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6044 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-31majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6043 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6042 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6041 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6040 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6039 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6038 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-26Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make ↵herbelin
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
2004-08-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6036 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6035 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6033 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Expansion du prédicat du 'match' vis à vis de la dépendance en le terme ↵herbelin
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
2004-08-24Prise en compte expansion du prédicat du 'match' vis à vis de la ↵herbelin
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
2004-08-24Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6030 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Deplacement des fonctions de typage des predicate de Cases a la V7 de ↵herbelin
inductiveops vers pretyping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6029 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Calling setoid_rewrite on a term H whose type (eq x y) was not an applicationsacerdot
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
2004-08-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6027 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23Précisions message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6026 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23Interpretation et affichage corrects des notations LetTuple, affichage des ↵herbelin
notations If git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6025 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23Pas de notation v7 si purement en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6023 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23Correction bug #830 : les noms des implicites temporaires étaient inconnus ↵herbelin
au moment de l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6021 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23The previous test file was truncated. New commit to fix the previoussacerdot
commit error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6020 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-06Amélioration message d'erreur objet de récursion de type non inductifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6019 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-06Apply implicit types to local binders tooherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6017 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Header V8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6016 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Protection contre un indice d'evar égal à 0herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6015 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Zbool déjà dans ZArith_baseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6013 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Minimisation utilisation NNPPherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6012 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Déclaration d'obsolescenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6011 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6010 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Refherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6009 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Bug indexation des Require Importherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6006 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-01Commentaires coqdocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6004 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-01Commentaires coqdocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6001 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-30Protection erreur find_eq_data dans decompEqThen et uniformisation messages ↵herbelin
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
2004-07-30MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5998 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-30Unbind the macosx dmg after creation to be able to build it again safelyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5997 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5996 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5995 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-29Distinction location ocaml 3.08 ou pas (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5993 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-29MAJ cible patchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5991 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-29Protection unlocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5990 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-29Distinction location ocaml 3.08 ou pasherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5987 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-29Bug join_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5985 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5983 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-28Bug tactique fixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5981 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5980 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-27Utilisation de la variable camlp4 OCAML_308 plutôt que d'en reconstruire ↵herbelin
une nous-mêmes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5979 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-08 19:21:34 +0000