aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_constrnew.ml4
AgeCommit message (Collapse)Author
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵herbelin
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
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
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
2005-09-21Niveau 99 permettant de parser { } nécessaire aussi dans l'entrée patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7394 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-04Ajout explicite du niveau 200 de pattern auquel on fait référence au ↵herbelin
niveau 0; nécessaire pour option -nois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7109 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-24Passage d'une bibliothèque de grands entiers naturels vers une ↵herbelin
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
2004-11-17Déclaration de '..' comme mot-clé (résoud bug #856)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6316 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5570 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Utilisation de '..' pour la notation concrete des motifs recursifs de filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5517 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Mise en place de motifs récursifs dans Notation; quelques simplifications ↵herbelin
au passage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5510 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts ↵barras
fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-26Keep structure information for Fixpoint declaration and Fix termsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
- 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
2004-01-26reparation de qqs bugs du traducteurbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5248 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-13Reference obsolete au niveau 200 de patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5196 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16MAJ suppression 250herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5105 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-08correction bug: parentheses ne cassent plus les implicitesbarras
on met la notation ( _ ) qu'autour des entiers positifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5078 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-04Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace ↵herbelin
par un niveau ajoute dynamiquement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5068 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-23Prise en compte des definitions locales dans les (co-)points-fixesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4974 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Suppression des niveaux videsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4968 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Distinction entre 'as _' qui cache le terme filtre (si variable) et rien ↵herbelin
dans case_item git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4949 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18reparation bug moins unaire (erreur de PP)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4944 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-17Inteprétation des idents filtrés liants dans constrintern.ml (plus robuste)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4927 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Bug parsing castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4899 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵barras
Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12petits changements de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Fusion de tuple_constr/tuple_pattern dans operconstr/patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4832 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Utilisation de niveaux pour l'extensibilite de la grammaires des patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4759 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ↵herbelin
associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 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-17On n'autorise plus les niveaux doubles L/R en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4670 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-15Mise en conformite return_type en fonction de la docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4643 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11mise a jour nouvelle syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 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-09-26Syntaxe plus liberale pour le type des arguments de filtrage du 'match'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4491 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-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵herbelin
choix du parseur en fonction de cette option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4387 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Passage des projections au niveau 1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4349 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-06Passage de lconstr à constr pour les arguments immédiat de commandesherbelin
et tactiques; qqes bugs d'affichage; passage de la précédence des projections de 10 à 9 avec associativité à gauche git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4312 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Ajout token '!' pour correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4269 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-11Token '.(' seulement pour v8, sinon conflit avec '.(*'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4137 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵herbelin
les metavariables de patterns; fusion NoHypId et Hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Factorisation des produits de même type; parenthèses autour des x:=c et ↵herbelin
n:=c dans les 'with bindings' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3974 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 07:41:44 +0000