aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Collapse)AuthorAge
* revision de la semantique de rewrite ... in <clause>. details dans la docGravatar letouzey2006-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de comportement du [rewrite ... in H]: Coq échoue si HGravatar notin2006-10-03
| | | | | | | | apparaît dans le but ou dans l'une des hypothèses (ferme les bugs #447, #883 et #1228). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9201 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retour sur la suppression du pf_nf (trop d'exemples utilisent avecGravatar herbelin2006-10-03
| | | | | | | | | | profit la simplification des arguments -- même si dans quelques cas trop de réduction obligent à revenir en arrière). Remplacement par un hack rapide (et non "scalable"). Suppression code mort oublié commit précédent sur equality.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur l'injection et la discrimination...Gravatar herbelin2006-10-01
| | | | | | | | | | | | | | | | | | Efficacité: - remplacement du typage par du re-typage léger - suppression d'un pf_nf suspect (cf bug #1173) [quid de la compatibilité ?] - remplacement des tests aveugles de projection impossible par un test qui vérifie au fur et à mesure que les filtrages sont autorisés Réorganisation: - factorisation des parties communes de injEq/discrEq/decompEq (à noter l'ordre inverse de génération des équations dans inj et decomp...) - uniformisation des noms "e" et "ee" utilisés dans la construction des combinateurs de discrimination Extension: - ajout d'une clause "as" à injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9195 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de la comparaison (inutile) des paramètres globaux desGravatar herbelin2006-09-30
| | | | | | | | | | | | constructeurs dans la recherche des positions de divergence entre expressions construites (possible source d'inefficacité d'injection/discriminate dans le cas de paramètres globaux convertibles mais syntaxiquement distincts -- cf rapport de bug 1173, première suggestion, même si dans le cas soumis les paramètres sont syntaxiquement les mêmes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9193 85f007b7-540e-0410-9357-904b9bb8a0f7
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
| | | | | | | | | | | | 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
* Correcting for bug #1167 Gravatar jforest2006-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9010 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating documentation of replace and correcting a typo in error message of ↵Gravatar jforest2006-06-12
| | | | | | replace. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8950 85f007b7-540e-0410-9357-904b9bb8a0f7
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour ↵Gravatar herbelin2006-05-30
| | | | | | permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8878 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
| | | | | | | | | | | sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
* "subst." works now even when it exists an hypothesis have the form "x=x" in ↵Gravatar jforest2006-05-20
| | | | | | the goal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8835 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
| | | | | | | | | | | | | | | | | | | | | juste rewrite in <id>, on a maintenant rewrite in <clause>. Ainsi rewrite H in H1,H2 |- * === rewrite H in H1; rewrite H in H2; rewrite H Pour l'instant rewrite H in * |- signifie: faire une fois "try rewrite H in Hi" sur toutes les hypotheses Hi du contexte sauf H En particulier, n'echoue pour l'instant pas s'il n'y a rien a reecrire nulle part. NB: rewrite H in * === rewrite H in * |- * === rewrite H in * |- ; rewrite H ATTENTION: la syntaxe de rewrite ayant changé, j'adapte interface en conséquence. Est-ce la bonne facon de faire ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8780 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de comportement de rewrite: face a une egalité setoid, onGravatar letouzey2006-05-02
| | | | | | | | | | | | | | arrete de reduire brutalement pour essayer de tomber sur une egalité Coq. Au contraire, si la relation de tete est une relation declarée dans la base des setoids, on l'utilise. ATTENTION: ceci brise la compatibilité, dans le cas très improbable ou quelqu'un aurait defini un setoid mais exploiterait la "feature" de la reduction vers l'eventuelle egalité Coq sous-jacente. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8779 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 1119 (inversion marche a moitie dans Type)Gravatar herbelin2006-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8677 85f007b7-540e-0410-9357-904b9bb8a0f7
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
| | | | | | | | | | | destruct x y z using scheme + replace c1 with c2 <in hyp> has now a new optional argument <as tac> replace c1 with c2 by tac tries to prove c2 = c1 with tac + I've also factorize the code correspoing to replace in extractactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8651 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesGravatar herbelin2006-01-16
| | | | | | | | - New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns - TacTrueCut and TacForward merged into new TacAssert bound to Tactics.forward git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7875 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage coqlibGravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | 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
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Types inductifs parametriquesGravatar mohring2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation bug #1004; nettoyageGravatar herbelin2005-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7351 85f007b7-540e-0410-9357-904b9bb8a0f7
* essai de typage des instantiations d\'evarsGravatar barras2005-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7117 85f007b7-540e-0410-9357-904b9bb8a0f7
* Expansion Case dans injection et discriminate (cf bug #829)Gravatar herbelin2004-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6335 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'dependent rewrite in'Gravatar herbelin2004-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6265 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration fonctions de réécriture depuis égalité dépendante; ↵Gravatar herbelin2004-10-27
| | | | | | factorisation cut_replacing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6261 85f007b7-540e-0410-9357-904b9bb8a0f7
* New tactic [setoid_]rewrite ... in ... [generate side conditions ...].Gravatar sacerdot2004-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proof term size optimization: setoid_rewrite H where H is an application ofGravatar sacerdot2004-09-30
| | | | | | | | Leibniz equality and no side conditions are imposed by the user simply calls the rewrite tactic. This was already done for setoid_replace/replace. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6164 85f007b7-540e-0410-9357-904b9bb8a0f7
* New syntaxGravatar sacerdot2004-09-29
| | | | | | | | | | | "setoid_rewrite dir term generate side conditions constr_list" to specify a list of side conditions that must be a subset of the generated new goals. Used to disambiguate in case of multiple set of generated side conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6157 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug report #855Gravatar herbelin2004-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6125 85f007b7-540e-0410-9357-904b9bb8a0f7
* hiding the meta_map in evar_defsGravatar barras2004-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 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
* Since setoid_{replace,rewrite} now uses replace there is a circularityGravatar sacerdot2004-07-23
| | | | | | | | 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
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Message d'erreurGravatar herbelin2004-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5511 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug d'Inversion #529 (pb avec ordre d'evaluation)Gravatar barras2004-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5496 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retablissement de la correction bug d'inversion faite dans la version 1.116 ↵Gravatar herbelin2004-03-12
| | | | | | et malencontreusement passe a la trappe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de la distinction entre elimination de Type vers Type ou pas ↵Gravatar herbelin2004-03-11
| | | | | | (False, eq, Unit ont maintenant les bonnes proprietes pour fonctionner partout) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5454 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug de l'inversion (coq-bugs #529)Gravatar barras2004-03-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5444 85f007b7-540e-0410-9357-904b9bb8a0f7
* ne pas échouer si but inchangé pour préserver la compatibilité de 'replace'Gravatar herbelin2004-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5411 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction sur commit précédent : Tactics.cut réduisait de manière ↵Gravatar herbelin2004-03-01
| | | | | | inappropriée git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'replace in'Gravatar herbelin2004-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5408 85f007b7-540e-0410-9357-904b9bb8a0f7
* Blindage vis a vis des constructeurs partiellement appliquesGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4937 85f007b7-540e-0410-9357-904b9bb8a0f7
* factorisation et generalisation des clausesGravatar barras2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction semantique des InHyp de clause en InHypValue si local def; ↵Gravatar herbelin2003-11-09
| | | | | | simplification suite fusion eq/eqT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4840 85f007b7-540e-0410-9357-904b9bb8a0f7
* subst marche dans les deux sensGravatar filliatr2003-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4663 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation comportement decompEq pour corriger un bug introduit dans le ↵Gravatar herbelin2003-10-11
| | | | | | Inversion acceptant le nommage des hypotheses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4602 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-05 21:26:08 +0000