aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2008-08-21Fixes in dependent induction tactic to keep names, allow givingmsozeau
intro-patterns and avoid useless generalizations on inductive parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11331 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-05Correction de bugs:herbelin
- evarconv: mauvaise idée d'utiliser la conversion sur la tête d'un terme applicatif au moment de tester f u1 .. un = g v1 .. vn au premier ordre : on revient sur l'algo tel qu'il était avant le commit 11187. - Bug #1887 (format récursif cassé à cause de la vérification des idents). - Nouveau choix de formattage du message "Tactic Failure". - Nettoyage vocabulaire "match context" -> "match goal" au passage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11305 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-04Évolutions diverses et variées.herbelin
- Correction divers messages d'erreur - lorsque rien à réécrire dans une hyp, - lorsqu'une variable ltac n'est pas liée, - correction anomalie en présence de ?id dans le "as" de induction, - correction mauvais env dans message d'erreur de unify_0. - Diverses extensions et améliorations - "specialize" : - extension au cas (fun x1 ... xn => H u1 ... un), - renommage au même endroit. - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize". - "induction" - intro des IH toujours au sommet même si induction sur var quantifiée, - ajout d'un hack pour la reconnaissance de schémas inductifs comme N_ind_double mais il reste du boulot pour reconnaître (et/ou réordonner) les composantes d'un schéma dont les hypothèses ne sont pas dans l'ordre standard, - vérification de longueur et éventuelle complétion des intropatterns dans le cas de sous-patterns destructifs dans induction (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas le n dans le contexte), - localisation des erreurs d'intropattern, - ajout d'un pattern optionnel après "as" pour forcer une égalité et la nommer (*). - "apply" accepte plusieurs arguments séparés par des virgules (*). - Plus de robustesse pour clear en présence d'evars. - Amélioration affichage TacFun dans Print Ltac. - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !). - Fusion VTactic/VFun dans l'espoir. - Mise en place d'un système de trace de la pile des appels Ltac (tout en préservant certains aspects de la récursivité terminale - cf bug #468). - Tactiques primitives - ajout de "move before" dans les tactiques primitives et ajout des syntaxes move before et move dependent au niveau utilisateur (*), - internal_cut peuvent faire du remplacement de nom d'hypothèse existant, - suppression de Intro_replacing et du code sous-traitant - Nettoyage - Suppression cible et fichiers minicoq non portés depuis longtemps. (*) Extensions de syntaxe qu'il pourrait être opportun de discuter git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-28Fixes in generalize_eqs/dependent induction to allow the user to specifymsozeau
generalized variables himself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11280 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-28Fix wrong environment bug in test for setoid_rewrite or rewrite.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11279 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-28Fix bug in term dnet preventing some unifications. Allow "higher-order"msozeau
class constraints of the form Π x1 ... xn, Class args. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11278 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-26Even better test for choosing rewrite or setoid_rewrite.msozeau
Now there is a class "SetoidRelation" for registering relations that should always be considered as setoids and never unfolded. Every "Add Relation" command adds an instance and impl,iff are there by default. Now the test is: if there is a SetoidRelation instance, use it ; otherwise, allow unfolding to find an eq or fallback on setoid_rewrite. To avoid searching for SetoidRelation instances repeateadly we check that it is really needed first by unfolding the hyp. Only two scripts relied on the now-forbidden semantics of rewriting by an @eq inside a setoid relation, in Numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11269 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-25A better test for relations being setoids or not: do leibniz rewrite iffmsozeau
the applied relation is an abbreviation for @eq. Fixes bug #1915. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11264 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-25More compatibility fixes, revert the tauto fix that preventedmsozeau
destruction of records as a lot of scripts currently rely on it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11263 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24Tauto breaking not only binary "conjunctions" seems like a bad ideamsozeau
after all... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11259 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24A (safe) implementation of prolog's cut in the typeclasses eauto to avoidmsozeau
redoing proofs for nothing, i.e, do not backtrack on proofs whose evars are disjoint from the evars of the rest of the goals. Fixes the example in bug #1911, needs some more testing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11258 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24Suite commit 11236notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11252 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24Propagation de l'information "strict" (càd à toplevel ou en train deherbelin
définir une ltac) dans l'interprétation des identificateurs isolés en position de tactiques, comme dans "let x:=y in t" (résoud l'incompatibilité #1906). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11250 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-22New tactics [conv] to test convertibility (actually, unification) of twomsozeau
terms and [head_of_constr id] to put the head of a constr in some new hypothesis. Both are used in a new tactic to deal with partial applications in setoid_rewrite. Also fix bug #1905 by using [subrelation] to take care of [Morphism (R ==> R') id] constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11244 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-22A try at allowing matching on applications as a binary syntax node by default.msozeau
It breaks tauto as [?X _ _] matches much more terms. It is mostly fixed by not destructing objects of record types. The new [intuition] was also pulling an unneeded dependency in Field_theory which can be cleared easily. Zis_gcd_bezout is also considered a conjunction now, which seems correct(?). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11243 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵notin
de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-18Modification rapide du message d'erreur lorsqu'un _ ne peut êtreherbelin
effacé dans un intro-pattern (suggéré par ssreflect). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11235 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-16Quelques modifications autour du filtrage Ltac:herbelin
- Optimisation du filtrage sous-terme de Ltac (cf sub_match) pour le cas où c'est le n-ième sous-termes qui finalement réussit (passage à une complexité en n plutôt que n^2, via l'utilisation de continuations). - Sémantique du filtrage: suppression dans sub_match de la recherche dans le type des let (puisque ce n'est pas cencé être une information utilisateur) mais rajout de la recherche dans le champ cast qui lui est utilisateur. - Nouvelle fonctionnalité: récupération des noms des variables liantes filtrées (dans matches/sub_match) et utilisation de ces noms dans ltac (utile pour récupérer x dans "exists x, P x"); git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11226 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-07Fix implicit arguments in sections bug and check for resolution of evars whenmsozeau
defining records. Fix test-suite script because of new implicit argument setting for DefaultRelation. Fix regression in auto, changing the order of tried lemmas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11213 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-02Stop using the discrimination net in typeclasses/setoid rewrite, which wasmsozeau
considering every definition opaque by default, until a better fix is found. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11202 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
goals containing existentials and use transparency information on constants (optionally). Only used by the typeclasses eauto engine for now, but could be used for other hint bases easily (just switch a boolean). Had to add a new "creation" hint to be able to set said boolean upon creation of the typeclass_instances hint db. Improve the proof-search algorithm for Morphism, up to 10 seconds gained in e.g. Field_theory, Ring_polynom. Added a morphism declaration for [compose]. One needs to declare more constants as being unfoldable using the [Typeclasses unfold] command so that discrimination is done correctly, but that amounts to only 6 declarations in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11184 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de ↵notin
globalisation (add_glob* et dump_*) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-22Rename obligations_tactic to obligation_tactic and fix bugs #1893.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11164 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-21Correction petit bug sur révision 11159 (res_pf fait un effet de bordherbelin
sur le sigma, utilisation de refine à la place). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11162 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
discriminate/injection/simplify_eq acceptent maintenant un terme comme argument. Les clauses "with" et les variantes "e" sont aussi acceptées. Aussi, discriminate sans argument essaie maintenant toutes les hyps quantifiées (au lieu de traiter seulement les buts t1<>t2). --This line, and those below, will be ignored-- M doc/refman/RefMan-tac.tex M CHANGES M pretyping/evd.ml M pretyping/termops.ml M pretyping/termops.mli M pretyping/clenv.ml M tactics/extratactics.ml4 M tactics/inv.ml M tactics/equality.ml M tactics/tactics.mli M tactics/equality.mli M tactics/tacticals.ml M tactics/eqdecide.ml4 M tactics/tacinterp.ml M tactics/tactics.ml M tactics/extratactics.mli M toplevel/auto_ind_decl.ml M contrib/funind/invfun.ml M test-suite/success/Discriminate.v M test-suite/success/Injection.v M proofs/clenvtac.mli M proofs/clenvtac.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-19Little fixes: print unbound variable in error message (patch by Samuelmsozeau
Bronson), some keywords in coqdoc, and test well-typedness of predicate in subtac_cases after abstraction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11153 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-19incomplete bugfix for infocorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11149 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
(résolution entre autres des bugs 1882, 1883, 1884). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-18Fix bug in implementation of splitting of class constraints.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11141 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-18Compatibility fixes (Add Setoid bug and accidental introduction of amsozeau
tactic named "app"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11139 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-17Fixes w.r.t. let binders in class contexts and Add Parametricmsozeau
Morphism/Relation bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11132 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-17Better typeclass error messages, always giving the full set ofmsozeau
unsatisfiable constraints. Add a resolution call in tacinterp before trying the default tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11131 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-16Add possibility to match on defined hypotheses, using brackets tomsozeau
disambiguate syntax: [ H := [ ?x ] : context C [ foo ] |- _ ] is ok, as well as [ H := ?x : nat |- _ ] or [H := foo |- _ ], but [ H := ?x : context C [ foo ] ] will not parse. Add applicative contexts in tactics match, to be able to match arbitrary partial applications, e.g.: match f 0 1 2 with appcontext C [ f ?x ] => ... end will bind C to [ ∙ 1 2 ] and x to 0. Minor improvements in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11129 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-11Optionally (and by default) split typeclasses evars into connected msozeau
components and resolving them separately, reporting more precise failures. Improve error messages. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11105 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
- Changement au passage de la convention "at -n1 ... -n2" en "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut pas mélanger des positifs et des négatifs. - Au passage: - simplification de gclause avec fusion de onconcl et concl_occs, - généralisation de l'utilisation de la désignation des occurrences par la négative aux cas de setoid_rewrite, clrewrite et rewrite at, - correction d'un bug de "rewrite in at" qui utilisait le at de la conclusion dans les hyps. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11094 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-10- Correct handling of DependentMorphism error, using tclFAIL instead ofmsozeau
letting the exception go uncatched. - Reorder definitions in Morphisms, move the PER on (R ==> R') in Morphisms where it can be declared properly. Add an instance for Equivalence => Per. - Change bug#1604 test file to the new semantics of [setoid_rewrite at] - More unicode characters parsed by coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-10Backtrack sur l'"optimisation" de admit (révision 11084). Comme leherbelin
fait remarquer Bruno, c'est ne pas anodin de laisser croire qu'on admet une conjecture alors qu'on admet uniquement la conclusion de cette conjecture, conclusion qui peut être incohérente et qui ne le serait pas si on avait gardé le contexte du but. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11089 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-10- Correction bug 1841 (identificateurs incorrects avec Subclass)herbelin
- Correction wish 1866 (un "admit" plus fin dans sa généralisation des hyps) - Bricoles dans cases.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11085 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09- Correction de la version simplifiée (filtrage sur deux sigherbelin
imbriqués) du bug 1834, mais le bug 1834 reste ouvert [cases.ml]. - Réactivation de l'interprétation des listes dans "generalize" cassée depuis 11072) [tacinterp.ml]. - Bricoles et petit nettoyage en passant [cases.ml et g_vernac.ml4]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11083 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-08- Patch sur "intros until 0"herbelin
- MAJ CHANGES et COMPATIBILITY - Réservation de || et && dans Notations.v - code mort et MAJ suite commit 11072 (tactics.ml et changes.txt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11073 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
- Ajout clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute aussi une égalité pour se souvenir du terme sur lequel l'induction ou l'analyse de cas s'applique. - Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de Programs qui avait la sémantique de "pose proof" tandis que le nouveau a la même sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de noms dans Arith, et ajout EqNat dans Arith. - Documentation tactiques et notations de tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-07Correct handling of the environment in build_signature, and throwmsozeau
exception for dependent arrow types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11069 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-07Change setoid_rewrite's matching semantics to continue matching insidemsozeau
matched occurences that are not selected. Permit to rewrite at 3 different places in (a + b) + (c + d) = 0 with a lemma ending in [_ + _]. Order is depth-first and left-to-right. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11068 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
Minor fix in Morphisms which prevented working with higher-order morphisms and PER relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11065 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-05Correctly catch UnresolvableConstraint exception which is now located. msozeau
Fixes Sophia/Float. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11052 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03Fixes incorrect handling of existing existentials variables inmsozeau
typeclass code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11047 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
files, about definitions and type of references. - Add missing location information on fixpoints/cofixpoint in topconstr and syntactic definitions in vernacentries for correct dumping. - Dump definition information in vernacentries: defs, constructors, projections etc... - Modify coqdoc/index.mll to use this information instead of trying to scan the file. - Use the type information in latex output, update coqdoc.sty accordingly. - Use the hyperref package to do crossrefs between definition and references to coq objects in latex. Next step is to test and debug it on bigger developments. On the side: - Fix Program Let which was adding a Global definition. - Correct implicits for well-founded Program Fixpoints. - Add new [Method] declaration kind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-30Improve the dependent induction tactic to automatically find themsozeau
generalized hypotheses. Also move part of the tactic to ML and improve the generated proof term in case of non-dependent induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11023 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-23- Fix bug #1858, Hint Unfold calling the wrong locate function.msozeau
- Fix typeclass interface: instance_constructor now takes the instance constrs as argument to build and return the corresponding term and type. - Better typeclass error reporting when defining fixpoints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10975 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-12 03:31:13 +0000