aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface/xlate.ml
AgeCommit message (Collapse)Author
2008-02-01Unification de TacLetRecIn et TacLetIn. En particulier, on peutherbelin
maintenant écrire des fonctions récursives qui n'ont pas l'apparence d'être fonctionnelle. La sémantique reste toutefois différente. Par exemple, dans Ltac is := let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in i. l'évaluation de i est paresseuse, alors que dans une version non récursive Ltac is := let i := match goal with |- ?A -> ?B => intro | _ => idtac end in i. l'évaluation de i est forte (et échoue sur le "match" qui n'est pas autorisé à retourner une tactique). (note: code mort dans tactics.ml en passant + indexation Implicit Type dans doc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10495 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-18Change notation for setoid inequality, coerce objects before comparing them. ↵msozeau
Debug tactic redefinition code, streamline Instantiation Tactic implementation using that. Have to adapt obligations tactic still. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10449 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-07Completion of 10427...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10429 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-31Merged revisions ↵msozeau
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting des fonctions (à un ou deux arguments tous ou partie de type option). Il reste quelques opérations dans Util à propos desquelles je ne suis pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain car il est tard (comme some_in qui devrait devenir Option.make je suppose) . Elles s'expriment souvent facilement en fonction des autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y" . Le option_cons devrait faire son chemin dans le module parce qu'il est assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml. J'en ai profité aussi pour remplacer les trop nombreux "failwith" par des erreurs locales au module, donc plus robustes. J'ai trouvé aussi une fonction qui était définie deux fois, et une définie dans un module particulier. Mon seul bémol (mais facile à traiter) c'est la proximité entre le nom de module Option et l'ancien Options. J'ai pas de meilleure idée de nom à l'heure qu'il est, ni pour l'un, ni pour l'autre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-09Nettoyage de Print Assumptions :aspiwack
- Le code est maintenant mieux commenté. - J'ai aussi réorganisé un petit peu pour le rendre plus léger, mais presque rien - j'ai changé les noms internes : needed_assumptions devient assumptions et PrintNeededAssumptions devient PrintAssumptions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10311 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
Ajout de l'option with à (e)destruct et (e)induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-01Complément nécessaire aux révisions 10156 et 10157herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10158 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-28Modification of the Scheme command.vsiles
Now you can forget to provide the name of the scheme, it will be built automatically depending of the sorts involved. e.g. Scheme Induction for nat Sort Set. will build nat_rec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10148 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-30Oubli dans commit 10102...herbelin
+ Formattage affichage arguments evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10104 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06Adding a syntax for "n-ary" rewrite: letouzey
rewrite H, H' means: rewrite H; rewrite H'. This should still be compatible with other "features" of rewrite: like orientation, implicit arguments (t:=...), and "in" clause. Concerning the "in" clause, for the moment only one is allowed at the very end of the tactic, and it applies to all the different rewrites that are done. For instance, if someone _really_ wants to use all features at the same time: rewrite H1 with (t:=u), <-H2, H3 in * means: rewrite H1 with (t:=u) in *; rewrite <- H2 in *; rewrite H3 in * git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9954 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06sequel to commit 9952: forgot to adapt xlate to the new n-ary renameletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9953 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06New intro pattern "@A", which generates a fresh name based on A.glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9950 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26killing some more non-exhaustive patternsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9912 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-25Modification of VernacScheme to handle a new scheme: Equality (equality invsiles
boolean, will be added later) and update so everything is fine with the new syntax. New Type: type scheme = | InductionScheme of bool * lreference * sort_expr | EqualityScheme of lreference ... | VernacScheme of (lident * scheme) list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9860 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
discussion avec Georges) - La notion d'insertion maximale n'est plus globale mais attachée à chaque implicite - Correction de petits bugs dans le calcul des implicites - Raffinement de la notion "sous contexte" pour l'affichage des coercions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-29Ajout possibilité d'options à trois mots.herbelin
Suppression au passage syntaxe "Set table field ref", synonyme de "Add table field ref" et de "Unset table field ref", synonyme de "Remove table field ref". Changement de la syntaxe "Test tabel field val" en ""Test tabel field for val". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9810 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-28Ajout de la possibilité de faire référence dans certains cas à un nomherbelin
par sa notation (p.ex. pour unfold ou pour lazy delta). Ex: Goal 3+4 = 7. unfold "+". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9804 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-28Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.herbelin
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in", "erewrite" et "erewrite in". Correction au passage des bugs #1461 et #1522). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
delta-reduction at fonctor application. Example: Module Type S. Parameter Inline N : Set. End S. Module F (X:S). Definition t := X.N. End F. Module M. Definition N := nat. End M. Module G := F M. Print G.t. G.t = nat : Set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-02Extension to the general sequence operator (tactical). Now in addition to ↵emakarov
the form expr_0 ; [ expr_1 | ... | expr_n ] where expr_i could be empty, expr_i may be ".." or "expr ..". Note that "..." is a part of the metasyntax while ".." is a part of the object syntax. It may be necessary to enclose expr in parentheses. There may be at most one expr_i ending with "..". The number of expr_j not ending with ".." must be less than or equal to the number of subgoals generated by expr_0. The idea is that if expr_i is "expr .." or "..", then the value of expr (or idtac in case "..") is applied to as many intermediate subgoals as necessary to make the number of tactics equal to the number of subgoals. More precisely, if expr_0 generates n subgoals then the command expr_0; [expr_1 | ... | expr_i .. | ... | expr_m], where 1 <= i <= m, applies (the values of) expr_1, ..., expr_{i-1} to the first i - 1 subgoals, expr_i to the next n - m + 1 subgoals, and expr_{i+1}, ..., expr_m to the last m - i subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9742 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-19Forgot to update to new castmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9719 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-24Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9678 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-29Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9550 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
- Makefile: Option (environment variable NO_RECOMPILE_LIB) to not recompile the whole standard library just because the coq binaries got rebuilt. - Infrastructure to change the object pretty-printers at runtime. - Use that infrastructure to make coqtop-protocol with Pcoq trees and Pcoq-protocol with pretty-printed terms possible in coq-interface. - Make "Back(track)" into closed sections, modules and module types "Just Work™". - Modernise/generalise Pcoq protocol a bit, make some of its warts optional. - Implement "Show." in Pcoq mode. - Add Rpow_def.vo to REALSBASEVO so that its dependencies are computed (and used). - "make revision" now handles GNU Arch / tla in addition to svn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
- Avant : une unique méthode discharge_function qui avait accès à l'ancien environnement mais pas de possibilité de raisonner avec les objets du nouvel environnement en cours de construction. C'était problématique pour le discharge des implicites, arguments scope, etc qui étaient finalement faits en même temps que le discharge des constantes et inductifs mais avec pour effets de bord que les entrées dans la lib_stk arrivaient juste avant celles des constantes et inductifs avec des problèmes pour effacer les bonnes entrées au moment du reset - Maintenant : deux méthodes distinctes : discharge_function qui est appliquée pour collecter de l'ancien environnement ce qui est à garder dans la section et rebuild_function qui reconstruit le nouvel environnement connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant l'extensibilité que la méthode ancienne du fichier discharge.ml ne permettait pas) Au passage, ajout d'un modificateur Global aux déclarations d'implicites et d'arguments scopes pour indiquer qu'elles doivent perdurer à la sortie de la section Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps discharged reste) Au passage, nettoyage impargs.ml, suppression code mort résiduel du traducteur etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9474 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-11Changement dans le kernel : bgregoir
- essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-24Extension de fresh (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9272 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-01Une passe sur l'injection et la discrimination...herbelin
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
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-09-20Declarative Proof Language: main commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Ajout possibilité clause "where" dans co-points fixes herbelin
(+ uniformisation position notation dans les blocs inductifs et récursifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9110 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22making otags working jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9075 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-07-06Suite remplacement VernacDebug par VernacSetOptionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9023 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-03Extension des motifs disjonctifs au cas de disjonction de motifs multiplesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Suite passage ident -> hyp dans syntaxe de 'replace with in'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8981 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Changement du type d'argument 'TacticArgType X' en un typeherbelin
'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de pouvoir typer correctement les wit_tactic (auparavant le typage des wit_tactic était trop libéral et permettait de casser la subject-reduction). Amélioration au passage de l'affichage de la tactique "replace by" (module Extratactics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8926 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Détection bug rawwit suitecorrection trou de typage create_argherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8919 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour ↵herbelin
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
2006-05-02Extension syntaxique de rewrite in: au lieu de pouvoir faire letouzey
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
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-14Si un fixpoint a plusieurs arguments, mais un seul de type inductif, letouzey
ce patch dispense d'ecrire le { struct .. } En pratique, dans Topconstr.fixpoint_expr et Rawterm.fix_kind, l'index de l'argument inductif devient un int option au lieu d'un int. Les deux cas possibles: - Some n : les situations autorisées auparavant, a savoir {struct} explicite, ou bien un seul argument au total - None : le cas nouveau, qui redonne un entier lors du passage de rawconstr à constr si l'on trouve effectivement un unique argument ayant un type inductif, et une erreur sinon. Pour l'instant, on cherche l'inductif dans le type de manière syntaxique, mais il est jouable de rajouter un poil de reduction (au moins delta). Dans le détail, voici les coins que ce patch influence: - parsing/g_xml.ml4: continue pour l'instant a attendre un index explicite via un element xml "recIndex" - contrib/interface/xlate.ml: a priori ca marche, car il y avait déjà un cas ctv_ID_OPT_NONE correspondant à l'absence de struct. Par contre, dans le détail, le code pour un CFix utilise l'index de recurrence pour recouper au besoin le type du fixpoint en deux. Est-ce que je me gourre en supposant que si l'on a besoin de couper ainsi ce type, c'est qu'il provient non pas du parseur Coq, mais de l'impression d'un constr, et donc que l'index aura été correctement résolu ? - contrib/subtac/subtac_command.ml: - contrib/funind/indfun.ml: dans les deux cas, j'ai fait le service minimum, le struct reste obligatoire s'il y a plusieurs arguments. Mais ca ne serait pas dur à adapter pour ceux qui comprennent ces parties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8718 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-21+ destruct now works as induction on multiple arguments : jforest
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
2006-03-13Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.msozeau
May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-10induction now admits multiple induction arguments. The principle mustcoq
be explicitely given, and ALL parameters and args of the scheme must be given (only branches must be omitted). For the moment, only principle like generated by GenFixpoint (functional induction) are usable. That is the predicate must have a additional paramter like in: (P x1 ... xn (f p1...pm x1...xn)) Example of use : induction x y (add x y) using add_ind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8023 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-28Ajout option 'using lemmas' à auto/trivial/eautoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7937 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Suppression code pour hints nommés à la V7 (voire à la V6...)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7936 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et ↵herbelin
fail peuvent maintenant être des listes de string, int et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7908 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 01:19:50 +0000