aboutsummaryrefslogtreecommitdiff
path: root/tactics/setoid_replace.ml
AgeCommit message (Collapse)Author
2007-02-24Une passe sur les warnings (ajout Options.warn déclenchée par ↵herbelin
compile-verbose + ajout Pp.strbrk pour faciliter les césures faciles + messages divers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-22Ajout fonction clenv_conv_leq pour résoudre les pbs de la formeherbelin
"R ?1 ... ?n <= T". Utilisation de cette fonction dans Setoid_replace au au lieu de w_unify (suggestion de GG). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9673 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-19Raffinement de l'unification de "apply": mémorisation de certainsherbelin
degrés de liberté concernant les instances de méta (cumulativité et possibilité d'éta-expansion) de telle sorte que la fusion d'équations se fasse modulo ces degrés de liberté. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9389 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-01Quick hack to solve to complexity issue in function mark_occurherbelin
(but should probably not work in presence of morphisms to Leibniz's equality). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9331 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-31Retour sur la modification apportée en r9289, et nouvelle correction du bug ↵notin
#1259 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9328 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-26Affichage d'un message d'erreur losque qu'une relation n'a pas été ↵notin
déclarée (Setoid_replace.find_relation_class) (ferme le bug #1259) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9289 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-20Correction du bug #1255 (réécriture setoid sous un produit)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9253 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
InType) for "replace <c1> with <c2>" and "replace c1" and partially for "autorewrite". + Adding a "by tactic" optional argument to "setoid_replace". + Fixing bug #1207 + Add new test files for syntax change and updating doc. + Moving argument tactic extensions from extratactics to extraargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9073 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06reparation pour le bug #1072 (soufflee par J. Forest): letouzey
protection d'un list_chop pour couvrir le cas d'une application partielle de morphisme. accessoirement, il faudrait comprendre un jour pourquoi setoid replace inspecte (and True) dans le terme (map (and True) True <-> A) si on lui dit de reecrire A en autre chose... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8900 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-05encore un correctif sur le rewrite H in setoid: letouzey
si H: a==b, alors ce rewrite echouait lorsque a apparait dans b ou b dans a. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8788 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Standardisation nom option_app en option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses letouzey
avec des equivalences parametrees (genre forall n, P n <-> Q n) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8683 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵herbelin
G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24New commit to allow definitions of morphisms on relations whose carrier issacerdot
a Prod. Example: m : feq ==> feq where m has type (A -> B) -> (C -> D) and few is a relation over (fun X Y: Type. X -> Y). The problem is to avoid the interpretation (A -> B) -> C -> D that tries to use feq over D and feq over C considering (A -> B) as a quantification. This closes a wish of Bas Spitters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7068 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-19Setoid_replace: improved error message when trying to replace a term in asacerdot
non-applicative context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7040 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-19A wish by Bas Spitters granted: a little more of unification up tosacerdot
convertibility is now tried in setoid_rewrite. As a consequence it is now possible to declare relations over the function space (fun A B: Type => A -> B). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7039 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-18Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of thesacerdot
term to be replaced in the term that is the morphism was done too early (before computing the "morphism family" parameters). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6605 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-17Bug fixed (reported by Roland): the setoire_rewrite in tactic did not worksacerdot
in the followin case: H : t < c1 H0: c1 < c2 ============= t' setoid_rewrite H0 in H Explanation: the tactic made a cut with H0: c1 < c2 =============== t < c2 and then did setoid_rewrite <- H0 in H. If c2 occurs in t, then the tactic may fail (due to wrong variance). The simple fix consists in changing "t < c2" to "let H := c2 in t{H/c2} < c2" and then perform an intro before proceeding. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6601 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
the new module kernel/mod_subst.ml. MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now possible to define substitutions that also delta-expand constants (by associating the delta-expanded form to the constant name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-12Changement dans les boxed values .gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-27Factorisation cut_replacingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6263 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-25Word "setoid" banned from the error messages. "relation" used instead.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6255 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-25Missing check implemented (closes a bug from Bas Spitters).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6253 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-21The morphism lemma type was simplified only in modules and not in modulesacerdot
types. Fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6249 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-21Error message improved.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6248 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20The bug already closed in revision 1.90 was reintroduced again.sacerdot
Closed again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6243 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-19Proof term size reduction (again).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6241 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18* Code simplification and clean-up. In particular there is no more codesacerdot
duplicated between add_relation and add_setoid. * Less ad-hoc backward compatibility lemmas for setoids required in Setoid.v * Term size reduction (first part): when a relation is registered, we add to the environment a definition that gives back either the relation as an argument or as a relation class. The definition is used to reduce the term size. [ Note: we could save a bit more by defining two definitions in place of one. However, we suppose that the lambda term fragments generated can be shared quite effectively. Thus we would recive almost no benefit by sharing in terms of size. What about proof checking time? ] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6238 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18Code simplification and clean-up.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6237 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18The lem field was not computed properly for morphisms whose argument wassacerdot
a quantified Leibniz relation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6236 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18The "lem" field of a morphism used to be the compatibility proof, but itsacerdot
became the whole structure of type Morphism_Theory. A new field morphism_theory has now been added to record both informations. Print Setoids now prints again the right information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6235 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18Bug fixed: relations quantified more than once where abstracted in the wrongsacerdot
order (and thus they were not accepted). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6234 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18More informative error message when the tactic tries to generate a newsacerdot
goal with metavariables in it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6233 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-18zeta flag added to reduce LetIns in a morphism type. Morphisms with localsacerdot
definitions in their types are now accepted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6232 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-15Wrong comment committed. The tactic behaves correctly only when thesacerdot
relation/morphisms are quantified using LetIns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6222 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-15Wish of Maggesi implemented: the type of the morphism compatibility lemmasacerdot
is now the one that is shown to the user (and not only convertible to it). In this way it is possible to register the lemma in the Hint database. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6217 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14Bug fixed (reported by Maggesi): sometimes when the tactic had to generate newsacerdot
existential variables it failed. Fixing by propagating the metavariable environment generated by the unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6215 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14Code clean-up.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6214 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14reflexivity, symmetry, symmetry ... in e transitivity now fall-backsacerdot
to their setoid_* counterparts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6213 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07setoid_symmetry in ... implemented.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6194 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07New commandssacerdot
setoid_reflexivity setoid_symmetry setoid_transitivity The command setoid_symmetry in ... is not implemented yet (it behaves just as symmetry in ... for now). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6193 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07Now Print Setoids prints also the transitivity justification of transitivesacerdot
relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6191 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-06* New syntactic sugar: Add Relation ... transitivity proved by ...sacerdot
now declares both the relation and the relation as a morphism, computing the appropriate signature (depending on the reflexivity of the relation). * New parameter "as ..." to Add Relation (to be able to compute the morphism name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6189 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-04 20:27:18 +0000