aboutsummaryrefslogtreecommitdiffhomepage
path: root/translate
Commit message (Collapse)AuthorAge
* Ajout constructeur External pour appel outil externe à CoqGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6680 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout constructeur External pour appel outil externe à CoqGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la syntaxe du reset label: "BackTo n".Gravatar coq2005-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6590 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
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵Gravatar herbelin2005-01-02
| | | | | | printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
* ExtraRedExpr maintenant sans argument: pas très souple mais au moins ↵Gravatar herbelin2004-12-29
| | | | | | convient pour l'exemple de MapleMode qui lui ne passait pas quand un argument était exigé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6526 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@6499 85f007b7-540e-0410-9357-904b9bb8a0f7
* pp of nested fixpoints (dangling with/for)Gravatar barras2004-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6387 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export pr_intro_patternGravatar herbelin2004-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6385 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
* Ajout 'Locate Module'Gravatar herbelin2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6320 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage des universGravatar herbelin2004-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6276 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs ↵Gravatar herbelin2004-10-12
| | | | | | sont autorisés avant l'énoncé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6207 85f007b7-540e-0410-9357-904b9bb8a0f7
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the ↵Gravatar herbelin2004-10-11
| | | | | | evaluation of tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de or-pattern pour le match-with v8Gravatar herbelin2004-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 85f007b7-540e-0410-9357-904b9bb8a0f7
* "Print Setoids" command added.Gravatar sacerdot2004-07-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction vis à vis du type loc pour compatibilité ocaml 3.08Gravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5932 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
* 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
* Plus de robustesse en traduisant les 'Repeat Induction' et les 'Do n Induction'Gravatar herbelin2004-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5786 85f007b7-540e-0410-9357-904b9bb8a0f7
* pb facto des Fixpoint + erreur avec -dump-glob et LoadGravatar barras2004-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chgt role 2eme argument AList et implantation affichage motifs recursifs de ↵Gravatar herbelin2004-04-08
| | | | | | notations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5663 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction ad hoc pour Hint Rewrite in usingGravatar herbelin2004-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5533 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hack pour traduction des changements non uniformes de syntaxe des TACTIC et ↵Gravatar herbelin2004-03-17
| | | | | | VERNAC EXTEND (e.g. Hint Rewrite) [2eme] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5526 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hack pour traduction des changements non uniformes de syntaxe des TACTIC et ↵Gravatar herbelin2004-03-17
| | | | | | VERNAC EXTEND (e.g. Hint Rewrite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5525 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de motifs récursifs dans Notation; quelques simplifications ↵Gravatar herbelin2004-03-17
| | | | | | au passage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5510 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug inversion abstract_constr_expr et prod_constr_exprGravatar herbelin2004-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5471 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
* Retablissement pour le traducteur d'une copie de pr_intro_pattern base sur ↵Gravatar herbelin2004-03-05
| | | | | | la copie traduisante de pr_id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5434 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'Gravatar herbelin2004-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de natural en int_or_var pour 'do' et 'fail' pour ↵Gravatar herbelin2004-03-02
| | | | | | paramétrisation dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5418 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
* 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
* Keep structure information for Fixpoint declaration and Fix termsGravatar bertot2004-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
* commit précédent erronéGravatar herbelin2004-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs/insuffisances trouvees en traduisant MModeGravatar herbelin2004-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5361 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
* Suppression de 'Print.' en v8Gravatar herbelin2004-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5265 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation de qqs bugs du traducteurGravatar barras2004-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5248 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrige: Intros [] etait traduit intros (), qui ne reparse pasGravatar barras2004-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables ↵Gravatar herbelin2004-01-13
| | | | | | a b:A' et 'Variables (a:A) (b:A)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5198 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
* certains id n'etaient pas renommes pour eviter les conflits avec les mots-clesGravatar barras2004-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5172 85f007b7-540e-0410-9357-904b9bb8a0f7
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 07:20:10 +0000