aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/xlate.ml
Commit message (Collapse)AuthorAge
* Extension de fresh (suite)Gravatar herbelin2006-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9272 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
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout possibilité clause "where" dans co-points fixes Gravatar herbelin2006-09-01
| | | | | | | (+ 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
* making otags working Gravatar jforest2006-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9075 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
* Suite remplacement VernacDebug par VernacSetOptionGravatar herbelin2006-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9023 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension des motifs disjonctifs au cas de disjonction de motifs multiplesGravatar herbelin2006-07-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite passage ident -> hyp dans syntaxe de 'replace with in'Gravatar herbelin2006-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8981 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
| | | | | | | | | | | | | | '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
* Détection bug rawwit suitecorrection trou de typage create_argGravatar herbelin2006-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8919 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
* 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
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* + 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
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
| | | | | | | | 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
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
| | | | | | | | | | | | | 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
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7937 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression code pour hints nommés à la V7 (voire à la V6...)Gravatar herbelin2006-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et ↵Gravatar herbelin2006-01-21
| | | | | | 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
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser CoqGravatar herbelin2006-01-16
| | | | | | | | choisir un nom; utilisation de IntroAnonymous au lieu de None dans l'argument "with_names" des tactiques induction, inversion et assert. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7880 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
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux ↵Gravatar herbelin2005-12-30
| | | | | | de chaîne de caractères tel que "foo" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7762 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵Gravatar herbelin2005-12-26
| | | | | | 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
* Achèvement suppression traducteur dans contrib/interfaceGravatar herbelin2005-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7712 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
* adds the the case VernacShow(ShowMatch _) in the pattern-matching construct,Gravatar bertot2005-11-14
| | | | | | | but only maps to an error message. Avoid warnings about unused variables. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7561 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command: "Print Ltac qualid" to print user defined tactics.Gravatar sacerdot2005-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7053 85f007b7-540e-0410-9357-904b9bb8a0f7
* added VernacBacktrack (new backtracking command dedicated toGravatar coq2005-05-19
| | | | | | | | interfaces like PG, coqied or pcoq) in order to get rid of a pattern matching not exhaustive. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7038 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵Gravatar herbelin2005-05-17
| | | | | | aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow auto to have a parametric argument (wish #967)Gravatar herbelin2005-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added 'clear - id' to clear all hypotheses except the ones dependent in the ↵Gravatar herbelin2005-03-07
| | | | | | statement of id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renaming Print Canonical Structure into Print Canonical ProjectionsGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Print Canonical StructuresGravatar herbelin2005-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout cas VernacBackToGravatar herbelin2005-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6641 85f007b7-540e-0410-9357-904b9bb8a0f7
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
| | | | | | | "T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6582 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
| | | | | | | | | | | | | | | | | * "Module X [binders] [:T] [:= b]." is now used to define a module both in module definitions and module type definitions. Moreover "b" can now be a functor application in every situation (this was not accepted for module definitions in module type definitions) * "Declare Module X : T." is now used to declare a module both in module definitions and module type definitions. - Added syntactic sugar "Declare Module Export/Import" and "Module Export/Import" - Added syntactic sugar "Module M(Export/Import X Y: T)" and "Module Type M(Export/Import X Y: T)" (only for interactive definitions) (doc TODO) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6564 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage d'une bibliothèque de grands entiers naturels vers une ↵Gravatar herbelin2004-12-24
| | | | | | bibliothèques de grands entiers relatifs munis des 4 opérations de base git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6501 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restauration type casted_open_constr pour tactique refine car l'unification ↵Gravatar herbelin2004-12-09
| | | | | | n'est pas assez puissante pour retarder la coercion vers le but au dernier moment git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
* Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des ↵Gravatar herbelin2004-12-06
| | | | | | tactiques d'appliquer une éventuelle coercion vers le but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction 1.138 appliquée à tort à la branche principale au lieu de ↵Gravatar herbelin2004-11-29
| | | | | | V8-0bugfix; retour version 1.137 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6379 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commit précédent erroné; retour version précédenteGravatar herbelin2004-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6377 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ vis à vis de extratacticsGravatar herbelin2004-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6368 85f007b7-540e-0410-9357-904b9bb8a0f7
* Locate ModuleGravatar herbelin2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6325 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 19:23:00 +0000