aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-09-03Bug List.hd vs list_lastherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6056 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03MAJ options coqtop et coqcherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6053 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03* New test (for setoid_replace in the general case)sacerdot
* Comments/to do changed (but still in italian) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6052 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03* setoid_test.v removed and added again in new syntaxsacerdot
* setoid_test.v8 ported to the new implementation of setoid_*. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6051 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03Ported to the new implementation of setoid_*.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6050 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03New reflexive implementation of setoid_rewrite. The new implementationsacerdot
introduces a few backward incompatibilities: 1. setoid_replace used to try to close the new goal using full_trivial. The new implementation does not try to close the goal. To fix the script it is sufficient to add a "; [ idtac | trivial ]." after every application of setoid_replace that used to generate just one goal. 2. (setoid_replace c1 c2) used to replace either c1 with c2 or c2 with c1 (if c1 did not occur in the goal). The new implementation only replaces c1 with c2. To fix the script it is sufficient to replace (setoid_replace c1 with c2) with (setoid_replace c1 with c2) || (setoid_replace c2 with c1) in those cases where it is unknown what should be substituted with what. 3. the goal generated by the "Add Morphism" command has the hypothesis permutated w.r.t. the old implementation. I.e. the old implementation used to generate: forall x1 x2, forall x3 x4, x1=x2 -> x3=x4 -> ... whereas the new implementation generates forall x1 x2, x1=x2 -> forall x3 x4, x3 = x4 -> ... Fixing the script is usually trivial. 4. the "Add Morphism P" command used to generate a non-standard goal in the case of P being a predicate (i.e. a function whose codomain is Prop). In that case the goal ended with an implication (instead of ending with a coimplication). The new implementation generates a standard goal that ends with a coimplication. To fix the script you can add the following line at the very beginning: cut <<old_goal>>; intro Hold; split; apply Hold; assumption || (symmetry;assumption). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6049 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03New command "Add Relation ..." (for the new implementation of setoid_*).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6048 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03The old implementation of (setoid_replace c1 with c2) used to replacesacerdot
either c1 with c2 or c2 with c1 (if c1 did not occur in the goal). The new implementation will not do it. Thus I am replacing every occurrence of (setoid_replace c1 with c2) with (setoid_replace c1 with c2 || setoid_replace c2 with c1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6047 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 13:19:57 +0000