aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:Gravatar sacerdot2004-07-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* 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
* Setoid_replace.setoid_replace last argument (that was supposed to be alwaysGravatar sacerdot2004-07-23
| | | | | | | None) removed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5970 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
* Abstraction vis a vis de dummy_locGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5915 85f007b7-540e-0410-9357-904b9bb8a0f7
* syntax compatibility fixGravatar corbinea2004-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5861 85f007b7-540e-0410-9357-904b9bb8a0f7
* instantiate entry: constr -> lconstrGravatar corbinea2004-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5856 85f007b7-540e-0410-9357-904b9bb8a0f7
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
* more evar stuffGravatar corbinea2004-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la coercion id dans context vers evaluable constant (bug #777)Gravatar herbelin2004-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5841 85f007b7-540e-0410-9357-904b9bb8a0f7
* effective evar refiningGravatar corbinea2004-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5827 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #787 de RolandGravatar barras2004-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5783 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarify the distinction between quantified_hypothesis and ↵Gravatar herbelin2004-06-02
| | | | | | declared_or_quantified_hypothesis; fixed the interpretation of the hyp in with-bindings, intro until, simple destruct and simple induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5782 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug mauvais sigmaGravatar herbelin2004-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Terminologie plus intuitive: evaluable -> unfoldableGravatar herbelin2004-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5716 85f007b7-540e-0410-9357-904b9bb8a0f7
* Morphismes déclarés comme Lemma pas comme DefinitionGravatar herbelin2004-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Distinction entre declarations internes (p.ex. _subproof) et declarations ↵Gravatar herbelin2004-03-30
| | | | | | utilisateurs pour export xml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5609 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur commit 1.20Gravatar herbelin2004-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5531 85f007b7-540e-0410-9357-904b9bb8a0f7
* Desactivation de la syntaxe v7 de Hint Rewrite en v8Gravatar herbelin2004-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5527 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
* Nouvelle reparation pour Abstract en presence de variables de contexte: on ↵Gravatar herbelin2004-03-15
| | | | | | considere une var de but comme var de contexte si elle a meme nom, meme type, et, le cas echeant meme corps git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur la réparation de Abstract qui casse autre chose; le problème ↵Gravatar herbelin2004-03-13
| | | | | | en présence de variables de section est plus subtil et sa résolution est reportée git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5473 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
* Ne pas ajouter le contexte de section dans Abstract, il est deja inclus ↵Gravatar herbelin2004-03-12
| | | | | | (avec possibles modifications par clear) dans le contexte de but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5468 85f007b7-540e-0410-9357-904b9bb8a0f7
* code obsoleteGravatar herbelin2004-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5455 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
* Ajout tactiques stepl et stepr de NimègueGravatar herbelin2004-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5447 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug internalisation 'context'Gravatar herbelin2004-03-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5446 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
* modif des fixpoints pour que si on donne une notation au produit, les pts ↵Gravatar barras2004-03-05
| | | | | | fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les ↵Gravatar herbelin2004-03-02
| | | | | | noms d'hypothèses; Changement de natural en int_or_var pour 'do' et 'fail' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5420 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les ↵Gravatar herbelin2004-03-02
| | | | | | noms d'hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5419 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id ↵Gravatar herbelin2004-03-02
| | | | | | variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5415 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
* Déplacement définition intro_pattern_expr dans GenargGravatar herbelin2004-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5406 85f007b7-540e-0410-9357-904b9bb8a0f7
* Généralisation du type ltac Identifier en IntroPattern; prise en compte ↵Gravatar herbelin2004-03-01
| | | | | | des IntroPattern au parsing, à l'interprétation, à la traduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5405 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement définition intro_pattern_expr dans GenargGravatar herbelin2004-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5404 85f007b7-540e-0410-9357-904b9bb8a0f7
* added breakpoints to help ideGravatar corbinea2004-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5387 85f007b7-540e-0410-9357-904b9bb8a0f7
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
| | | | | | | | | - fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5331 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus d'explicitation d'un message d'erreurGravatar herbelin2004-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5330 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
| | | | | | | | dans le module de leur définition. Internalisation des preident comme des noms qui ne sont pas des références git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5326 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug (destruct/induction ne savent pas traiter le cas non atomique avec ↵Gravatar herbelin2004-01-27
| | | | | | paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug induction lors de types inductives avec parametresGravatar herbelin2004-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5241 85f007b7-540e-0410-9357-904b9bb8a0f7
* bugs avec Pose et AssertGravatar barras2004-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation incompatibilites v7/v8 dans destruct; utilisation de noms t2_3 ↵Gravatar herbelin2003-12-23
| | | | | | dans induction/destruct qui marche maintenant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5137 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5134 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 15:22:53 +0000