aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2004-07-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5978 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5977 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5976 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-24Plus de pa_ifdef dans CAMLP4EXTENDFLAGSherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5975 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5974 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23Several tests for the bug-fixed and improved new version ofsacerdot
setoid_{replace,rewrite}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5973 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:sacerdot
1. setoid and morphisms declaration were used to become in scope only when a module is imported (and to disappear when a module is closed). Thus it was possible to declare a setoid in a module A; a morphism on it in a module B that imports A; and to write a module C that imports B (but not A) that uses the morphism. Since the morphism is in scope but the setoid isn't this was a source of bugs. Fixed by making the setoid/morphisms declaration always in scope (i.e. they become in scope when the module is loaded, not when it is imported). 2. since it is possible to define different setoids for the same type / different morphisms on the same function in separate modules and since it is possible to import them at once, we must allow the possibility to have more than one setoid for each type and more than one morphism for each function. The data structures of the tactic has been completely revised to allow this possibility. Right now warnings are used to highlight situations when an ambiguity is arised. In the near future syntax will be added to disambiguate the situation, and smart algorithms to find the right interpretations when more than one applies but only a few are succesfull. For the moment the choice of the interpretation (i.e. the association of a morphism to each function in the goal) is already done before the actual start of the tactic (in order to allow a modular implementation of the choice of the interpretation). 3. the tactic used to work only in those situations where all the functions involved in the path(s) root of the term - term(s) to replace were morphisms. In the case where they are simple functions (i.e. the ``default setoid'' is Leibniz) the tactic failed. These cases are now considered by making the setoid_replace tactic perform simple replace steps where needed. A future optimization will allow to minimize the number of replace steps. The tactic should be 100% compatible with the old tactic, but for the situations that used to fail and are now succesfull. The declaration of setoids/morphisms can now also be succesfull where it used to fail. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5972 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23Since setoid_{replace,rewrite} now uses replace there is a circularitysacerdot
involving the two modules Equality and Setoid_replace. Resolved by making equality register the replace function to the Setoid_replace module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5971 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23Setoid_replace.setoid_replace last argument (that was supposed to be alwayssacerdot
None) removed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5970 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23Setoid_replace.setoid_replace: last argument (that was supposed to besacerdot
always None) removed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5969 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23"Print Setoids" command added.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5968 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23"Show Setoids" command added.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5967 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5966 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-22correction d'un bug de la tactique pour les semi setoid rings.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5965 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5964 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5963 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-20Minimisation de l'utilisation de pa_ifdef.cmo pour éviter les messages ↵herbelin
d'obsolescence de ocaml 3.08 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5962 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-20Abstraction vis à vis de dummy_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5961 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5960 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5959 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 04:19:09 +0000