aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
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-09-08Meilleur anglais (cf #841)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6076 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03deplacement de clenv vers pretypingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03premiere reorganisation de l\'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-26Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make ↵herbelin
depend en erreur; déplacement de pa_ifdef dans MMakefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6037 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23Précisions message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6026 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-29Distinction location ocaml 3.08 ou pas (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5993 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-29Distinction location ocaml 3.08 ou pasherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5987 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-28Bug tactique fixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5981 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23"Print Setoids" command added.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5968 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-20Abstraction vis à vis de dummy_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5961 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Abstraction vis à vis du type loc pour compatibilité ocaml 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5932 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Suppression quotifyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5922 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-07-16Branchement sur Util.loc et abstraction vis a vis de dummy_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5912 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Abstraction vis a vis de dummy_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5910 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13bugs #667 and #783 (mimick_evar and loc_table on large files)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5894 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29moved instantiate binding to extratacticscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29efficacite du lexeurfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5847 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28more evar stuffcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-17Nouvelle syntaxe à la ML pour donner le type ML des extensions d'argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5815 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-03Affichage de l'opacité par About mais pas par Print (compatibilité coq'art)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5802 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Affichage de l'opacité dans Print et Aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5793 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-27Bug affichage ClearBodyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5771 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-14Bug syntaxe AddPathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5747 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Ajout entree pour exporter les commentaires en mode -xmlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5574 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-17Hack pour traduction des changements non uniformes de syntaxe des TACTIC et ↵herbelin
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
2004-03-17Hack pour traduction des changements non uniformes de syntaxe des TACTIC et ↵herbelin
VERNAC EXTEND (e.g. Hint Rewrite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5525 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Parsing des V8Notation avec motif recursif en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5520 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-03-03Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5426 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les ↵herbelin
noms d'hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5419 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Changement de natural en int_or_var pour 'do' et 'fail' pour ↵herbelin
paramétrisation dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5418 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-02Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id ↵herbelin
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
2004-03-02Correction oubli du cas pas d'arguments implicites du toutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5414 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-01Généralisation du type ltac Identifier en IntroPattern; prise en compte ↵herbelin
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
2004-02-28Expansion du type par nécessité dans le cas d'affichage d'implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5398 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-21Correction oubli de report d'une modification de g_vernac (1.69) vers ↵herbelin
g_vernacnew git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5371 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-02-17Ajout de lconstr, constr et binder_constr dans Print Grammar constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5355 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-16export the general function for getting information from the environmentbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5347 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-13Uniformisation du comportement de Notation et Reserved Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5341 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
dans le module de leur définition. Error_in_file dans Util et étendu avec possibilité de noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29Suppression de 'Print.' en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5265 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-27Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5253 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-18 21:57:33 +0000