aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface/xlate.ml
AgeCommit message (Collapse)Author
2004-02-12Implicits can have an optional list of argument, which is differentbertot
from an empty list of arguments. in H at 2 |- * was badly translated in clauses (for replacement tactics) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5318 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-02adds the possibility to mark function arguments as formulas in Ltacbertot
uncapitalizes dependentrewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5277 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-30updates the definition of tactics using Ltac and adds the subst tacticbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5274 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-30adds module commands and update the extration commandbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5273 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29Réutilisation de VernacSyntacticDefinition pour différencier "Notation id ↵herbelin
:= c" de "Notation "'id'" := c" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5264 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29updates the tactics contradiction and autorewrite, the commandsbertot
set implicit arguments, hint rewrite, and proof git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5263 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-28make sure that 'in' clauses for reduction tactics are translatedbertot
once again re-organize the way intro patterns are translated: there is now only one kind of pattern that can be used for both and and or constructs: the use of the multiplet notation should only be a matter of notation. un-capitalize a few tactic names for tactics represented using the TacExtend construct. corrects a bug in the way binders or coercion binders were used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5260 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-26a try to make intro patterns betterbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5247 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-24streamlines the keywords for definitions, require commandsbinders, notationbertot
definitions, Show commands, Print commands, proof starting commands, Search commands, scope commands, type reservation command, locate commands, time git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5244 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22change add path commands to get the extra argument and the Hint commandsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5239 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22fixes argument lists for tactic definitions, updates inversion tacticsbertot
so that they use intro-pattern-lists like induction and destruct git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5236 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22adds a clause argument to symmetrybertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5235 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22corrects the way the structural argument declaration is handled inbertot
fixpoint definitions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5234 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22adds the notations in inductive definitions, improves the consistency betweenbertot
induction et destruct, takes the extra argument for fail and idtac into account git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5233 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-22handles explicit function calls, names meta variables in patternsbertot
(in V8 the name is not a number), explicitation of arguments with names (but not with rank anymore), the refine tactic now has its own operator the structure information for hypotheses in induction is now handled as in intro, the tactic instantiate has been modified to use clauses, the wildcard rule for Ltac pattern matching on goals has been added and the possibility to refer to types of values and instantiated contexts in values in Ltac have been added. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5232 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-21updates the structure of fix (struct argument added) and ifbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5225 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-19handles projector notations, cases with return types,bertot
tuple lets, and a few tactics whose name appears with an upper case initial git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5218 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-19adds constructs to handle notations in patternsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5215 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-15translation to structures now okay for pattern matching constructsbertot
The locations in simpl, unfold, and the like are also better taken into account git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5209 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-14compact nested universal quantifications into a single quantification withbertot
a list of binders git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5204 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-13Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables ↵herbelin
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
2004-01-09bugs avec Pose et Assertbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-02meilleure presentation des commentaires du traducteurbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-01Nouvelle tactique EExistsclrenard
Changement des exports pour tactic EXTEND : with_bindings devient bindings qui prend plus le with, il faut le mettre à la main dans la règle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5052 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25Uniformisation des politiques de nommage de NewDestruct sur arguments ↵herbelin
recursifs et Induction style Hrec; mise en place systeme de traduction automatique; Elim/Case reconnaissent les premisses nommees du but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4989 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18correction suite ajout nouvelles tactiquesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4945 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-15Ajout Print Implicit avec depliage du typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4919 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13factorisation et generalisation des clausesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Bug TacIdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4884 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10Suppression SearchNamed finalement redondant avec SearchAboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4852 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4842 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-06Added Instantiate ... incorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Ajout CPatNotation, PrintVisibilityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4766 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4710 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16nouvelle syntaxe de ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4610 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Cablage en dur de inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4578 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10changement nouvelle syntaxe (pt fixes)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé ↵herbelin
incomplètement prouvé comme axiome git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4543 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4506 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Utilisation de noms dans 'Implicit Arguments [...]'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4459 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Mise en place d'implicites par noms en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19parsingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4416 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4369 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
records git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4322 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4319 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19Ajout 'Symmetry in Hyp'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4186 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 08:47:11 +0000