aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfilliatr1999-09-08 13:54:35 +0000
committerfilliatr1999-09-08 13:54:35 +0000
commitcfba911ee7f12c68e24b2d8db2cee08d6c6713ff (patch)
tree79bc8e510194dad127dbc818624dc8501be75d33
parent6560ae848fbc6a60e432d48d85fbbf12a8d2e6aa (diff)
compilation des grammaires (ouf)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@57 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--.depend24
-rw-r--r--Makefile24
-rw-r--r--parsing/g_basevernac.ml4135
-rw-r--r--parsing/g_command.ml450
-rw-r--r--parsing/g_multiple_case.ml414
-rw-r--r--parsing/g_prim.ml424
-rw-r--r--parsing/g_tactic.ml4210
-rw-r--r--parsing/g_vernac.ml4264
-rw-r--r--parsing/lexer.mll7
-rw-r--r--parsing/pcoq.ml4124
-rw-r--r--parsing/q_coqast.ml42
11 files changed, 442 insertions, 436 deletions
diff --git a/.depend b/.depend
index 1012d69001..b01304e337 100644
--- a/.depend
+++ b/.depend
@@ -175,6 +175,14 @@ toplevel/minicoq.cmx: kernel/constant.cmx parsing/g_minicoq.cmi \
kernel/names.cmx lib/pp.cmx kernel/sign.cmx \
/usr/local/lib/camlp4/stdpp.cmi kernel/term.cmx kernel/typing.cmx \
lib/util.cmx
+parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi \
+ /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi
+parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx \
+ /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi
+parsing/g_command.cmo: parsing/ast.cmi parsing/coqast.cmi \
+ /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi
+parsing/g_command.cmx: parsing/ast.cmx parsing/coqast.cmx \
+ /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi
parsing/g_minicoq.cmo: kernel/generic.cmi /usr/local/lib/camlp4/gramext.cmi \
/usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmi kernel/names.cmi \
lib/pp.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
@@ -183,13 +191,29 @@ parsing/g_minicoq.cmx: kernel/generic.cmx /usr/local/lib/camlp4/gramext.cmi \
/usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmx kernel/names.cmx \
lib/pp.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
parsing/g_minicoq.cmi
+parsing/g_multiple_case.cmo: parsing/ast.cmi parsing/coqast.cmi \
+ /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi
+parsing/g_multiple_case.cmx: parsing/ast.cmx parsing/coqast.cmx \
+ /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi
parsing/g_prim.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \
parsing/pcoq.cmi
parsing/g_prim.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/gramext.cmi \
parsing/pcoq.cmi
+parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi \
+ /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi lib/pp.cmi
+parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx \
+ /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi lib/pp.cmx
+parsing/g_vernac.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \
+ parsing/pcoq.cmi
+parsing/g_vernac.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/gramext.cmi \
+ parsing/pcoq.cmi
parsing/pcoq.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/gramext.cmi \
/usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmi lib/pp.cmi \
lib/util.cmi parsing/pcoq.cmi
parsing/pcoq.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/gramext.cmi \
/usr/local/lib/camlp4/grammar.cmi parsing/lexer.cmx lib/pp.cmx \
lib/util.cmx parsing/pcoq.cmi
+parsing/q_coqast.cmo: parsing/coqast.cmi /usr/local/lib/camlp4/mLast.cmi \
+ parsing/pcoq.cmi /usr/local/lib/camlp4/quotation.cmi
+parsing/q_coqast.cmx: parsing/coqast.cmx /usr/local/lib/camlp4/mLast.cmi \
+ parsing/pcoq.cmi /usr/local/lib/camlp4/quotation.cmi
diff --git a/Makefile b/Makefile
index eae9baaa29..581d751464 100644
--- a/Makefile
+++ b/Makefile
@@ -42,7 +42,9 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
LIBRARY=library/libobject.cmo library/summary.cmo
-PARSING=parsing/lexer.cmo parsing/pcoq.cmo parsing/ast.cmo
+PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
+ parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \
+ parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo
OBJS=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PARSING)
@@ -94,20 +96,28 @@ tags:
parsing/lexer.cmo: parsing/lexer.ml
$(OCAMLC_P4O) -c $<
+beforedepend:: parsing/lexer.ml
+
# grammar modules with camlp4
parsing/q_coqast.cmo: parsing/q_coqast.ml4
$(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o q_MLast.cmo -impl" -impl $<
-GRAMMAROBJS=parsing/coqast.cmo parsing/lexer.cmo parsing/pcoq.cmo \
- parsing/q_coqast.cmo parsing/g_prim.cmo
+parsing/g_prim.cmo: parsing/g_prim.ml4
+ $(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o pa_extend.cmo -impl" -impl $<
+
+GRAMMAROBJS=./lib/pp_control.cmo ./lib/pp.cmo ./lib/util.cmo ./lib/dyn.cmo \
+ ./lib/hashcons.cmo ./parsing/coqast.cmo ./parsing/lexer.cmo \
+ ./parsing/pcoq.cmo ./parsing/q_coqast.cmo ./parsing/g_prim.cmo
parsing/grammar.cma: $(GRAMMAROBJS)
- $(OCAMLC) $(BYTEFLAGS) -linkall -a -o $@
+ $(OCAMLC) $(BYTEFLAGS) $(GRAMMAROBJS) -linkall -a -o $@
-parsing/g_command.cmo: parsing/g_command.ml4
+parsing/g_%.cmo: parsing/g_%.ml4 parsing/grammar.cma
$(OCAMLC) $(BYTEFLAGS) -c -pp "camlp4o -I parsing pa_extend.cmo grammar.cma -impl" -impl $<
+beforedepend:: $(GRAMMAROBJS)
+
# Default rules
.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4
@@ -152,11 +162,11 @@ cleanconfig::
# Dependencies
-depend:
+depend: beforedepend
$(OCAMLDEP) $(DEPFLAGS) */*.mli */*.ml > .depend
for f in */*.ml4; do \
file=`dirname $$f`/`basename $$f .ml4`; \
- camlp4o $(INCLUDES) pa_extend.cmo pr_o.cmo -impl $$f > $$file.ml; \
+ camlp4o $(INCLUDES) pa_extend.cmo q_MLast.cmo $(GRAMMAROBJS) pr_o.cmo -impl $$f > $$file.ml; \
ocamldep $(DEPFLAGS) $$file.ml >> .depend; \
rm -f $$file.ml; \
done
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index f06f9228a7..2c8cb53dc3 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -1,27 +1,14 @@
-(****************************************************************************)
-(* The Calculus of Inductive Constructions *)
-(* *)
-(* Projet Coq *)
-(* *)
-(* INRIA ENS-CNRS *)
-(* Rocquencourt Lyon *)
-(* *)
-(* Coq V6.3 *)
-(* Jul 10th 1997 *)
-(* *)
-(****************************************************************************)
-(* g_basevernac.ml4 *)
-(****************************************************************************)
-(* camlp4o pa_extend.cmo ./q_ast.cma *)
+(* $Id$ *)
+
+open Coqast
+open Pcoq
-open CoqAst;;
-open Pcoq;;
+open Vernac
-open Vernac;;
GEXTEND Gram
identarg:
- [ [ id = LIDENT -> <:ast< ($VAR $id) >> ] ]
+ [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ]
;
ne_identarg_list:
[ [ l = LIST1 identarg -> l ] ]
@@ -64,79 +51,79 @@ GEXTEND Gram
[ [ l = ne_stringarg_list -> <:ast< (VERNACARGLIST ($LIST $l)) >> ] ]
;
vernac:
- [ [ LIDENT "Pwd"; "." -> <:ast< (PWD) >>
- | LIDENT "Cd"; "." -> <:ast< (CD) >>
- | LIDENT "Cd"; dir = stringarg; "." -> <:ast< (CD $dir) >>
+ [ [ IDENT "Pwd"; "." -> <:ast< (PWD) >>
+ | IDENT "Cd"; "." -> <:ast< (CD) >>
+ | IDENT "Cd"; dir = stringarg; "." -> <:ast< (CD $dir) >>
| "Quit"; "." -> <:ast< (QUIT) >>
- | LIDENT "Drop"; "." -> <:ast< (DROP) >>
- | LIDENT "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP) >>
- | LIDENT "Print"; LIDENT "All"; "." -> <:ast< (PrintAll) >>
- | LIDENT "Print"; "." -> <:ast< (PRINT) >>
- | LIDENT "Print"; LIDENT "Hint"; "*"; "."
+ | IDENT "Drop"; "." -> <:ast< (DROP) >>
+ | IDENT "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP) >>
+ | IDENT "Print"; IDENT "All"; "." -> <:ast< (PrintAll) >>
+ | IDENT "Print"; "." -> <:ast< (PRINT) >>
+ | IDENT "Print"; IDENT "Hint"; "*"; "."
-> <:ast< (PrintHint) >>
- | LIDENT "Print"; LIDENT "Hint"; s = identarg; "." ->
+ | IDENT "Print"; IDENT "Hint"; s = identarg; "." ->
<:ast< (PrintHintId $s) >>
- | LIDENT "Print"; LIDENT "Hint"; "." ->
+ | IDENT "Print"; IDENT "Hint"; "." ->
<:ast< (PrintHintGoal) >>
- | LIDENT "Print"; LIDENT "HintDb"; s = identarg ; "." ->
+ | IDENT "Print"; IDENT "HintDb"; s = identarg ; "." ->
<:ast< (PrintHintDb $s) >>
- | LIDENT "Print"; LIDENT "Section"; s = identarg; "." ->
+ | IDENT "Print"; IDENT "Section"; s = identarg; "." ->
<:ast< (PrintSec $s) >>
- | LIDENT "Print"; LIDENT "States"; "." -> <:ast< (PrintStates) >>
- | LIDENT "Locate"; LIDENT "File"; f = stringarg; "." ->
+ | IDENT "Print"; IDENT "States"; "." -> <:ast< (PrintStates) >>
+ | IDENT "Locate"; IDENT "File"; f = stringarg; "." ->
<:ast< (LocateFile $f) >>
- | LIDENT "Locate"; LIDENT "Library"; id = identarg; "." ->
+ | IDENT "Locate"; IDENT "Library"; id = identarg; "." ->
<:ast< (LocateLibrary $id) >>
- | LIDENT "Locate"; id = identarg; "." ->
+ | IDENT "Locate"; id = identarg; "." ->
<:ast< (Locate $id) >>
- | LIDENT "Print"; LIDENT "LoadPath"; "." -> <:ast< (PrintPath) >>
- | LIDENT "AddPath"; dir = stringarg; "." -> <:ast< (ADDPATH $dir) >>
- | LIDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >>
- | LIDENT "AddRecPath"; dir = stringarg; "." ->
+ | IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >>
+ | IDENT "AddPath"; dir = stringarg; "." -> <:ast< (ADDPATH $dir) >>
+ | IDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >>
+ | IDENT "AddRecPath"; dir = stringarg; "." ->
<:ast< (RECADDPATH $dir) >>
- | LIDENT "Print"; LIDENT "Modules"; "." -> <:ast< (PrintModules) >>
- | LIDENT "Print"; "Proof"; id = identarg; "." ->
+ | IDENT "Print"; IDENT "Modules"; "." -> <:ast< (PrintModules) >>
+ | IDENT "Print"; "Proof"; id = identarg; "." ->
<:ast< (PrintOpaqueId $id) >>
(* Pris en compte dans PrintOption ci-dessous
- | LIDENT "Print"; id = identarg; "." -> <:ast< (PrintId $id) >> *)
- | LIDENT "Search"; id = identarg; "." -> <:ast< (SEARCH $id) >>
- | LIDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >>
+ | IDENT "Print"; id = identarg; "." -> <:ast< (PrintId $id) >> *)
+ | IDENT "Search"; id = identarg; "." -> <:ast< (SEARCH $id) >>
+ | IDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >>
(* TODO: rapprocher Eval et Check *)
- | LIDENT "Eval"; r = Tactic.red_tactic; "in"; c = comarg; "." ->
+ | IDENT "Eval"; r = Tactic.red_tactic; "in"; c = comarg; "." ->
<:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c) >>
- | LIDENT "Eval"; g = numarg; r = Tactic.red_tactic;
+ | IDENT "Eval"; g = numarg; r = Tactic.red_tactic;
"in"; c = comarg; "." ->
<:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c $g) >>
| check = check_tok; c = comarg; "." -> <:ast< (Check $check $c) >>
| check = check_tok; g = numarg; c = comarg; "." ->
<:ast< (Check $check $c $g) >>
- | LIDENT "Print"; LIDENT "ML"; LIDENT "Path"; "." ->
+ | IDENT "Print"; IDENT "ML"; IDENT "Path"; "." ->
<:ast< (PrintMLPath) >>
- | LIDENT "Print"; LIDENT "ML"; LIDENT "Modules"; "." ->
+ | IDENT "Print"; IDENT "ML"; IDENT "Modules"; "." ->
<:ast< (PrintMLModules) >>
- | LIDENT "Add"; LIDENT "ML"; LIDENT "Path"; dir = stringarg; "." ->
+ | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = stringarg; "." ->
<:ast< (AddMLPath $dir) >>
- | LIDENT "Add"; LIDENT "Rec"; LIDENT "ML"; LIDENT "Path";
+ | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path";
dir = stringarg; "." ->
<:ast< (RecAddMLPath $dir) >>
- | LIDENT "Print"; LIDENT "Graph"; "." -> <:ast< (PrintGRAPH) >>
- | LIDENT "Print"; LIDENT "Classes"; "." -> <:ast< (PrintCLASSES) >>
- | LIDENT "Print"; LIDENT "Coercions"; "." -> <:ast< (PrintCOERCIONS) >>
- | LIDENT "Print"; LIDENT "Path"; c = identarg; d = identarg; "." ->
+ | IDENT "Print"; IDENT "Graph"; "." -> <:ast< (PrintGRAPH) >>
+ | IDENT "Print"; IDENT "Classes"; "." -> <:ast< (PrintCLASSES) >>
+ | IDENT "Print"; IDENT "Coercions"; "." -> <:ast< (PrintCOERCIONS) >>
+ | IDENT "Print"; IDENT "Path"; c = identarg; d = identarg; "." ->
<:ast< (PrintPATH $c $d) >>
-(* | LIDENT "Time"; "." -> <:ast< (Time) >>
- | LIDENT "Untime"; "." -> <:ast< (Untime) >> *)
+(* | IDENT "Time"; "." -> <:ast< (Time) >>
+ | IDENT "Untime"; "." -> <:ast< (Untime) >> *)
- | LIDENT "Time"; v = vernac -> <:ast< (Time $v)>>
- | LIDENT "SearchIsos"; com = comarg; "." ->
+ | IDENT "Time"; v = vernac -> <:ast< (Time $v)>>
+ | IDENT "SearchIsos"; com = comarg; "." ->
<:ast< (Searchisos $com) >>
- | "Set"; LIDENT "Undo"; n = numarg; "." ->
+ | "Set"; IDENT "Undo"; n = numarg; "." ->
<:ast< (SETUNDO $n) >>
- | LIDENT "Unset"; LIDENT "Undo"; "." -> <:ast< (UNSETUNDO) >>
- | "Set"; LIDENT "Hyps_limit"; n = numarg; "." ->
+ | IDENT "Unset"; IDENT "Undo"; "." -> <:ast< (UNSETUNDO) >>
+ | "Set"; IDENT "Hyps_limit"; n = numarg; "." ->
<:ast< (SETHYPSLIMIT $n) >>
- | LIDENT "Unset"; LIDENT "Hyps_limit"; "." ->
+ | IDENT "Unset"; IDENT "Hyps_limit"; "." ->
<:ast< (UNSETHYPSLIMIT) >>
(* Pour intervenir sur les tables de paramètres *)
@@ -145,30 +132,30 @@ GEXTEND Gram
<:ast< (SetTableField $table $field $value) >>
| "Set"; table = identarg; field = identarg; "." ->
<:ast< (SetTableField $table $field) >>
- | LIDENT "Unset"; table = identarg; field = identarg; "." ->
+ | IDENT "Unset"; table = identarg; field = identarg; "." ->
<:ast< (UnsetTableField $table $field) >>
| "Set"; table = identarg; value = option_value; "." ->
<:ast< (SetTableField $table $value) >>
| "Set"; table = identarg; "." ->
<:ast< (SetTableField $table) >>
- | LIDENT "Unset"; table = identarg; "." ->
+ | IDENT "Unset"; table = identarg; "." ->
<:ast< (UnsetTableField $table) >>
- | LIDENT "Print"; table = identarg; field = identarg; "." ->
+ | IDENT "Print"; table = identarg; field = identarg; "." ->
<:ast< (PrintOption $table $field) >>
(* Le cas suivant inclut aussi le "Print id" standard *)
- | LIDENT "Print"; table = identarg; "." ->
+ | IDENT "Print"; table = identarg; "." ->
<:ast< (PrintOption $table) >>
- | LIDENT "Add"; table = identarg; field = identarg; id = identarg; "."
+ | IDENT "Add"; table = identarg; field = identarg; id = identarg; "."
-> <:ast< (AddTableField $table $field $id) >>
- | LIDENT "Add"; table = identarg; id = identarg; "."
+ | IDENT "Add"; table = identarg; id = identarg; "."
-> <:ast< (AddTableField $table $id) >>
- | LIDENT "Test"; table = identarg; field = identarg; id = identarg; "."
+ | IDENT "Test"; table = identarg; field = identarg; id = identarg; "."
-> <:ast< (MemTableField $table $field $id) >>
- | LIDENT "Test"; table = identarg; id = identarg; "."
+ | IDENT "Test"; table = identarg; id = identarg; "."
-> <:ast< (MemTableField $table $id) >>
- | LIDENT "Remove"; table = identarg; field = identarg; id = identarg; "." ->
+ | IDENT "Remove"; table = identarg; field = identarg; id = identarg; "." ->
<:ast< (RemoveTableField $table $field $id) >>
- | LIDENT "Remove"; table = identarg; id = identarg; "." ->
+ | IDENT "Remove"; table = identarg; id = identarg; "." ->
<:ast< (RemoveTableField $table $id) >> ] ]
;
option_value:
@@ -177,9 +164,7 @@ GEXTEND Gram
| s = stringarg -> s ] ]
;
check_tok:
- [ [ LIDENT "Check" -> <:ast< "CHECK" >>
+ [ [ IDENT "Check" -> <:ast< "CHECK" >>
| "Type" -> <:ast< "PRINTTYPE" >> ] ] (* pas dans le RefMan *)
;
END;
-
-(* $Id$ *)
diff --git a/parsing/g_command.ml4 b/parsing/g_command.ml4
index 9066b77b5f..98b2d16e4a 100644
--- a/parsing/g_command.ml4
+++ b/parsing/g_command.ml4
@@ -7,7 +7,7 @@ open Command
GEXTEND Gram
ident:
- [ [ id = LIDENT -> <:ast< ($VAR $id) >> ] ]
+ [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ]
;
raw_command:
[ [ c = Prim.ast -> c ] ]
@@ -25,19 +25,19 @@ GEXTEND Gram
command0:
[ [ "?" -> <:ast< (XTRA "ISEVAR") >>
| "?"; n = Prim.number -> <:ast< (META $n) >>
- | "["; id1 = LIDENT; ":"; c = command; c2 = abstraction_tail ->
+ | "["; id1 = IDENT; ":"; c = command; c2 = abstraction_tail ->
<:ast< (LAMBDA $c [$id1]$c2) >>
- | "["; id1 = LIDENT; ","; idl = ne_ident_comma_list;
+ | "["; id1 = IDENT; ","; idl = ne_ident_comma_list;
":"; c = command; c2 = abstraction_tail ->
<:ast< (LAMBDALIST $c [$id1]($SLAM $idl $c2)) >>
- | "["; id1 = LIDENT; ","; idl = ne_ident_comma_list;
+ | "["; id1 = IDENT; ","; idl = ne_ident_comma_list;
c = abstraction_tail ->
<:ast< (LAMBDALIST (XTRA "ISEVAR") [$id1]($SLAM $idl $c)) >>
- | "["; id1 = LIDENT; c = abstraction_tail ->
+ | "["; id1 = IDENT; c = abstraction_tail ->
<:ast< (LAMBDA (XTRA "ISEVAR") [$id1]$c) >>
- | "["; id1 = LIDENT; "="; c = command; "]"; c2 = command ->
+ | "["; id1 = IDENT; "="; c = command; "]"; c2 = command ->
<:ast< (ABST #Core#let.cci $c [$id1]$c2) >>
- | "<<"; id1 = LIDENT; ">>"; c = command -> <:ast< [$id1]$c >>
+ | "<<"; id1 = IDENT; ">>"; c = command -> <:ast< [$id1]$c >>
| "("; lc1 = lcommand; ":"; c = command; body = product_tail ->
let id = Ast.coerce_to_var "lc1" lc1 in
<:ast< (PROD $c [$id]$body) >>
@@ -57,48 +57,48 @@ GEXTEND Gram
| "Prop" -> <:ast< (PROP {Null}) >>
| "Set" -> <:ast< (PROP {Pos}) >>
| "Type" -> <:ast< (TYPE) >>
- | LIDENT "Fix"; id = ident; "{"; fbinders = fixbinders; "}" ->
+ | IDENT "Fix"; id = ident; "{"; fbinders = fixbinders; "}" ->
<:ast< (FIX $id ($LIST $fbinders)) >>
- | LIDENT "CoFix"; id = ident; "{"; fbinders = cofixbinders; "}" ->
+ | IDENT "CoFix"; id = ident; "{"; fbinders = cofixbinders; "}" ->
<:ast< (COFIX $id ($LIST $fbinders)) >>
| v = ident -> v ] ]
;
command1:
- [ [ "<"; ":"; LIDENT "ast"; ":"; "<"; c = raw_command; ">>" -> c
- | "<"; l1 = lcommand; ">"; LIDENT "Match"; c = command; "with";
+ [ [ "<"; ":"; IDENT "ast"; ":"; "<"; c = raw_command; ">>" -> c
+ | "<"; l1 = lcommand; ">"; IDENT "Match"; c = command; "with";
cl = ne_command_list; "end" ->
<:ast< (XTRA "REC" $l1 $c ($LIST $cl)) >>
- | "<"; l1 = lcommand; ">"; LIDENT "Match"; c = command; "with"; "end"
+ | "<"; l1 = lcommand; ">"; IDENT "Match"; c = command; "with"; "end"
->
<:ast< (XTRA "REC" $l1 $c) >>
- | "<"; l1 = lcommand; ">"; LIDENT "Case"; c = command; "of";
+ | "<"; l1 = lcommand; ">"; IDENT "Case"; c = command; "of";
cl = ne_command_list; "end" ->
<:ast< (MUTCASE $l1 $c ($LIST $cl)) >>
- | "<"; l1 = lcommand; ">"; LIDENT "Case"; c = command; "of"; "end" ->
+ | "<"; l1 = lcommand; ">"; IDENT "Case"; c = command; "of"; "end" ->
<:ast< (MUTCASE $l1 $c) >>
- | LIDENT "Case"; c = command; "of"; cl = ne_command_list; "end" ->
+ | IDENT "Case"; c = command; "of"; cl = ne_command_list; "end" ->
<:ast< (XTRA "MLCASE" "NOREC" $c ($LIST $cl)) >>
- | LIDENT "Case"; c = command; "of"; "end" ->
+ | IDENT "Case"; c = command; "of"; "end" ->
<:ast< (XTRA "MLCASE" "NOREC" $c) >>
- | LIDENT "Match"; c = command; "with"; cl = ne_command_list; "end" ->
+ | IDENT "Match"; c = command; "with"; cl = ne_command_list; "end" ->
<:ast< (XTRA "MLCASE" "REC" $c ($LIST $cl)) >>
- | LIDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
+ | IDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
c = command; "in"; c1 = command ->
<:ast< (XTRA "MLCASE" "NOREC" $c (LAMBDALIST (XTRA "ISEVAR")
($SLAM $b $c1))) >>
- | LIDENT "let"; id1 = LIDENT ; "="; c = command; "in";
+ | IDENT "let"; id1 = IDENT ; "="; c = command; "in";
c1 = command -> <:ast< (ABST #Core#let.cci $c [$id1]$c1) >>
- | LIDENT "if"; c1 = command; LIDENT "then"; c2 = command;
- LIDENT "else"; c3 = command ->
+ | IDENT "if"; c1 = command; IDENT "then"; c2 = command;
+ IDENT "else"; c3 = command ->
<:ast< ( XTRA "MLCASE" "NOREC" $c1 $c2 $c3) >>
(* EN ATTENTE DE REMPLACER CE QUI EST DANS Program.v ... *)
| "<"; l1 = lcommand; ">";
- LIDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
+ IDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
c = command; "in"; c1 = command ->
<:ast< (MUTCASE $l1 $c (LAMBDALIST (XTRA "ISEVAR") ($SLAM $b $c1))) >>
| "<"; l1 = lcommand; ">";
- LIDENT "if"; c1 = command; LIDENT "then";
- c2 = command; LIDENT "else"; c3 = command ->
+ IDENT "if"; c1 = command; IDENT "then";
+ c2 = command; IDENT "else"; c3 = command ->
<:ast< (MUTCASE $l1 $c1 $c2 $c3) >>
| c = command0 -> c ] ]
;
@@ -131,7 +131,7 @@ GEXTEND Gram
[ [ c1 = command8 -> c1 ] ]
;
command10:
- [ [ "!"; f = LIDENT; args = ne_command9_list ->
+ [ [ "!"; f = IDENT; args = ne_command9_list ->
<:ast< (APPLIST (XTRA "!" ($VAR $f)) ($LIST $args)) >>
| f = command9; args = ne_command91_list ->
<:ast< (APPLIST $f ($LIST $args)) >>
diff --git a/parsing/g_multiple_case.ml4 b/parsing/g_multiple_case.ml4
index 4c20e3a279..6611911cad 100644
--- a/parsing/g_multiple_case.ml4
+++ b/parsing/g_multiple_case.ml4
@@ -8,7 +8,7 @@ open Command
GEXTEND Gram
pattern_list:
[ [ -> ([],[])
- | (id1,p) = pattern; (id2,pl) = pattern_list -> (id1@id2,[p :: pl]) ] ]
+ | (id1,p) = pattern; (id2,pl) = pattern_list -> (id1@id2, p::pl) ] ]
;
lsimple_pattern:
[ [ c = simple_pattern2 -> c ] ]
@@ -20,7 +20,7 @@ GEXTEND Gram
simple_pattern_list:
[ [ -> ([],[])
| (id1,p) = simple_pattern; (id2,pl) = simple_pattern_list ->
- (id1@id2,[p :: pl]) ] ]
+ (id1@id2, p::pl) ] ]
;
(* The XTRA"!" means we want to override the implicit arg mecanism of bdize,
since params are not given in patterns *)
@@ -28,7 +28,7 @@ GEXTEND Gram
[ [ (id1,p) = simple_pattern; (id2,lp) = pattern_list ->
(id1@id2, <:ast< (APPLIST (XTRA "!" $p) ($LIST $lp)) >>)
| (id1,p) = simple_pattern; "as"; id = ident ->
- ([Ast.nvar_of_ast id::id1], <:ast< (XTRA"AS" $id $p) >>)
+ ((Ast.nvar_of_ast id)::id1, <:ast< (XTRA"AS" $id $p) >>)
| (id1,c1) = simple_pattern; ","; (id2,c2) = simple_pattern ->
(id1@id2, <:ast< (APPLIST (XTRA "!" pair) $c1 $c2) >>) ] ]
;
@@ -37,20 +37,20 @@ GEXTEND Gram
;
ne_pattern_list:
[ [ (id1,c1) = pattern; (id2,cl) = ne_pattern_list ->
- (id1@id2, [c1 :: cl])
+ (id1@id2, c1::cl)
| (id1,c1) = pattern -> (id1,[c1]) ] ]
;
equation:
[ [ (ids,lhs) = ne_pattern_list; "=>"; rhs = command ->
let br =
- List.fold_right (fun s ast -> CoqAst.Slam loc (Some s) ast)
+ List.fold_right (fun s ast -> Coqast.Slam loc (Some s) ast)
ids
<:ast< (XTRA"EQN" $rhs ($LIST $lhs)) >> in
- let lid = List.map (fun s -> CoqAst.Id loc s) ids in
+ let lid = List.map (fun s -> Coqast.Id loc s) ids in
<:ast< (XTRA"LAMEQN"($LIST $lid) $br) >> ] ]
;
ne_eqn_list:
- [ [ e = equation; "|"; leqn = ne_eqn_list -> [e :: leqn]
+ [ [ e = equation; "|"; leqn = ne_eqn_list -> e :: leqn
| e = equation -> [e] ] ]
;
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 9ccc40ea3e..7be07ea0d1 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -10,10 +10,10 @@ GEXTEND Gram
GLOBAL: var ident number string path ast astpat astact entry_type;
var:
- [ [ s = LIDENT -> Nvar(loc,s) ] ]
+ [ [ s = IDENT -> Nvar(loc,s) ] ]
;
ident:
- [ [ s = LIDENT -> Id(loc,s) ] ]
+ [ [ s = IDENT -> Id(loc,s) ] ]
;
number:
[ [ i = INT -> Num(loc, int_of_string i) ] ]
@@ -25,23 +25,23 @@ GEXTEND Gram
[ [ (l,pk) = qualid -> Path(loc,l,pk) ] ]
;
qualid:
- [ [ "#"; l = LIST1 LIDENT SEP "#"; "."; pk = LIDENT -> (l, pk) ] ]
+ [ [ "#"; l = LIST1 IDENT SEP "#"; "."; pk = IDENT -> (l, pk) ] ]
;
(* ast *)
ast:
- [ [ id = LIDENT -> Nvar(loc,id)
+ [ [ id = IDENT -> Nvar(loc,id)
| s = INT -> Num(loc, int_of_string s)
| s = STRING -> Str(loc,s)
| p = path -> p
- | "{"; s = LIDENT; "}" -> Id(loc,s)
- | "("; nname = LIDENT; l = LIST0 ast; ")" -> Node(loc,nname,l)
+ | "{"; s = IDENT; "}" -> Id(loc,s)
+ | "("; nname = IDENT; l = LIST0 ast; ")" -> Node(loc,nname,l)
| "["; ido = idoption; "]"; b = ast -> Slam(loc,ido,b)
| "'"; a = ast -> Node(loc,"$QUOTE",[a]) ] ]
;
idoption:
[ [ "<>" -> None
- | id = LIDENT -> Some id ] ]
+ | id = IDENT -> Some id ] ]
;
(* meta-syntax entries *)
@@ -55,10 +55,10 @@ GEXTEND Gram
[ [ l = LIST0 ast -> Node loc "ASTLIST" l ] ]
;
action:
- [ [ LIDENT "let"; p = astlist; et = entry_type; "="; e1 = action; "in";
+ [ [ IDENT "let"; p = astlist; et = entry_type; "="; e1 = action; "in";
e = action -> Node(loc,"$CASE",[e1; et; Node(loc,"CASE",[p;e])])
- | LIDENT "case"; a = action; et = entry_type; "of";
- cl = LIST1 case SEP "|"; LIDENT "esac" ->
+ | IDENT "case"; a = action; et = entry_type; "of";
+ cl = LIST1 case SEP "|"; IDENT "esac" ->
Node(loc,"$CASE",a::et::cl)
| "["; al = astlist; "]" -> al ] ]
;
@@ -66,8 +66,8 @@ GEXTEND Gram
[[ p = astlist; "->"; a = action -> Node(loc,"CASE",[p;a]) ]]
;
entry_type:
- [[ ":"; LIDENT "List" -> Id(loc,"LIST")
- | ":"; LIDENT "Ast" -> Id(loc,"AST")
+ [[ ":"; IDENT "List" -> Id(loc,"LIST")
+ | ":"; IDENT "Ast" -> Id(loc,"AST")
| -> Id(loc,"AST") ]]
;
END
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a4e847c299..43ab29db3b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -13,11 +13,11 @@ open Tactic
GEXTEND Gram
identarg:
- [ [ id = LIDENT -> <:ast< ($VAR $id) >> ] ]
+ [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ]
;
numarg:
[ [ n = Prim.number -> n
- | "-"; n = Prim.number -> CoqAst.Num (Ast.loc n, ( - Ast.num_of_ast n))
+ | "-"; n = Prim.number -> Coqast.Num (Ast.loc n, ( - Ast.num_of_ast n))
] ]
;
comarg:
@@ -40,9 +40,9 @@ GEXTEND Gram
[ [ l = LIST1 pattern_occ -> l ] ]
;
pattern_occ_hyp:
- [ [ nl = ne_num_list; LIDENT "Goal" -> <:ast<(CCLPATTERN ($LIST $nl))>>
+ [ [ nl = ne_num_list; IDENT "Goal" -> <:ast<(CCLPATTERN ($LIST $nl))>>
| nl = ne_num_list; id = identarg -> <:ast<(HYPPATTERN $id ($LIST $nl))>>
- | LIDENT "Goal" -> <:ast< (CCLPATTERN) >>
+ | IDENT "Goal" -> <:ast< (CCLPATTERN) >>
| id = identarg -> <:ast< (HYPPATTERN $id) >> ] ]
;
ne_pattern_hyp_list:
@@ -82,7 +82,7 @@ GEXTEND Gram
binding_list:
[ [ c1 = comarg; ":="; c2 = comarg; bl = simple_binding_list ->
let id = match c1 with
- | CoqAst.Node(_,"COMMAND",[c]) -> coerce_to_var "c1" c
+ | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var "c1" c
| _ -> assert false
in <:ast<(BINDINGS (BINDING ($VAR $id) $c2) ($LIST $bl))>>
| n = numarg; ":="; c = comarg; bl = simple_binding_list ->
@@ -112,25 +112,25 @@ GEXTEND Gram
| p = unfold_occ -> [p] ] ]
;
red_flag:
- [ [ LIDENT "Beta" -> <:ast< (Beta) >>
- | LIDENT "Delta" -> <:ast< (Delta) >>
- | LIDENT "Iota" -> <:ast< (Iota) >>
+ [ [ IDENT "Beta" -> <:ast< (Beta) >>
+ | IDENT "Delta" -> <:ast< (Delta) >>
+ | IDENT "Iota" -> <:ast< (Iota) >>
| "["; idl = ne_identarg_list; "]" -> <:ast< (Unf ($LIST idl)) >>
| "-"; "["; idl = ne_identarg_list; "]" ->
<:ast< (UnfBut ($LIST idl)) >> ] ]
;
red_tactic:
- [ [ LIDENT "Red" -> <:ast< (Red) >>
- | LIDENT "Hnf" -> <:ast< (Hnf) >>
- | LIDENT "Simpl" -> <:ast< (Simpl) >>
- | LIDENT "Cbv"; s = LIST1 red_flag -> <:ast< (Cbv ($LIST s)) >>
- | LIDENT "Lazy"; s = LIST1 red_flag -> <:ast< (Lazy ($LIST s)) >>
- | LIDENT "Compute" -> <:ast< (Cbv (Beta) (Delta) (Iota)) >>
- | LIDENT "Unfold"; ul = ne_unfold_occ_list ->
+ [ [ IDENT "Red" -> <:ast< (Red) >>
+ | IDENT "Hnf" -> <:ast< (Hnf) >>
+ | IDENT "Simpl" -> <:ast< (Simpl) >>
+ | IDENT "Cbv"; s = LIST1 red_flag -> <:ast< (Cbv ($LIST s)) >>
+ | IDENT "Lazy"; s = LIST1 red_flag -> <:ast< (Lazy ($LIST s)) >>
+ | IDENT "Compute" -> <:ast< (Cbv (Beta) (Delta) (Iota)) >>
+ | IDENT "Unfold"; ul = ne_unfold_occ_list ->
<:ast< (Unfold ($LIST ul)) >>
- | LIDENT "Fold"; cl = comarg_list -> <:ast< (Fold ($LIST cl)) >>
- | LIDENT "Change"; c = comarg -> <:ast< (Change $c) >>
- | LIDENT "Pattern"; pl = ne_pattern_list ->
+ | IDENT "Fold"; cl = comarg_list -> <:ast< (Fold ($LIST cl)) >>
+ | IDENT "Change"; c = comarg -> <:ast< (Change $c) >>
+ | IDENT "Pattern"; pl = ne_pattern_list ->
<:ast< (Pattern ($LIST $pl)) >> ] ]
;
clausearg:
@@ -139,20 +139,20 @@ GEXTEND Gram
;
autoarg_depth:
[ [ n = numarg -> <:ast< $n>>
- | -> CoqAst.Str(loc,"NoAutoArg") ] ]
+ | -> Coqast.Str(loc,"NoAutoArg") ] ]
;
autoarg_adding:
- [ [ LIDENT "Adding" ; "["; l = ne_identarg_list; "]" ->
+ [ [ IDENT "Adding" ; "["; l = ne_identarg_list; "]" ->
<:ast< (CLAUSE ($LIST $l))>>
| -> <:ast< (CLAUSE) >> ] ]
;
autoarg_destructing:
- [ [ LIDENT "Destructing" -> CoqAst.Str(loc,"Destructing")
- | -> CoqAst.Str(loc,"NoAutoArg") ] ]
+ [ [ IDENT "Destructing" -> Coqast.Str(loc,"Destructing")
+ | -> Coqast.Str(loc,"NoAutoArg") ] ]
;
autoarg_usingTDB:
- [ [ "Using"; "TDB" -> CoqAst.Str(loc,"UsingTDB")
- | -> CoqAst.Str(loc,"NoAutoArg") ] ]
+ [ [ "Using"; "TDB" -> Coqast.Str(loc,"UsingTDB")
+ | -> Coqast.Str(loc,"NoAutoArg") ] ]
;
fixdecl:
[ [ id = identarg; n = numarg; ":"; c = comarg; fd = fixdecl ->
@@ -185,126 +185,126 @@ GEXTEND Gram
| st = simple_tactic -> st ] ]
;
simple_tactic:
- [ [ LIDENT "Fix"; n = numarg -> <:ast< (Fix $n) >>
- | LIDENT "Fix"; id = identarg; n = numarg -> <:ast< (Fix $id $n) >>
- | LIDENT "Fix"; id = identarg; n = numarg; "with"; fd = fixdecl ->
+ [ [ IDENT "Fix"; n = numarg -> <:ast< (Fix $n) >>
+ | IDENT "Fix"; id = identarg; n = numarg -> <:ast< (Fix $id $n) >>
+ | IDENT "Fix"; id = identarg; n = numarg; "with"; fd = fixdecl ->
<:ast< (Fix $id $n ($LIST $fd)) >>
- | LIDENT "Cofix" -> <:ast< (Cofix) >>
- | LIDENT "Cofix"; id = identarg -> <:ast< (Cofix $id) >>
- | LIDENT "Cofix"; id = identarg; "with"; fd = cofixdecl ->
+ | IDENT "Cofix" -> <:ast< (Cofix) >>
+ | IDENT "Cofix"; id = identarg -> <:ast< (Cofix $id) >>
+ | IDENT "Cofix"; id = identarg; "with"; fd = cofixdecl ->
<:ast< (Cofix $id ($LIST $fd)) >>
- | LIDENT "Induction"; s = identarg -> <:ast< (Induction $s) >>
- | LIDENT "Induction"; n = numarg -> <:ast< (Induction $n) >>
- | LIDENT "Double"; LIDENT "Induction"; i = numarg; j = numarg ->
+ | IDENT "Induction"; s = identarg -> <:ast< (Induction $s) >>
+ | IDENT "Induction"; n = numarg -> <:ast< (Induction $n) >>
+ | IDENT "Double"; IDENT "Induction"; i = numarg; j = numarg ->
<:ast< (DoubleInd $i $j) >>
- | LIDENT "Trivial" -> <:ast<(Trivial)>>
- | LIDENT "Trivial"; "with"; lid = ne_identarg_list ->
+ | IDENT "Trivial" -> <:ast<(Trivial)>>
+ | IDENT "Trivial"; "with"; lid = ne_identarg_list ->
<:ast<(Trivial ($LIST $lid))>>
- | LIDENT "Trivial"; "with"; "*" -> <:ast<(Trivial "*")>>
- | LIDENT "Auto"; n = numarg -> <:ast< (Auto $n) >>
- | LIDENT "Auto" -> <:ast< (Auto) >>
- | LIDENT "Auto"; n = numarg; "with";
+ | IDENT "Trivial"; "with"; "*" -> <:ast<(Trivial "*")>>
+ | IDENT "Auto"; n = numarg -> <:ast< (Auto $n) >>
+ | IDENT "Auto" -> <:ast< (Auto) >>
+ | IDENT "Auto"; n = numarg; "with";
lid = ne_identarg_list -> <:ast< (Auto $n ($LIST $lid)) >>
- | LIDENT "Auto"; "with";
+ | IDENT "Auto"; "with";
lid = ne_identarg_list -> <:ast< (Auto ($LIST $lid)) >>
- | LIDENT "Auto"; n = numarg; "with"; "*" ->
+ | IDENT "Auto"; n = numarg; "with"; "*" ->
<:ast< (Auto $n "*") >>
- | LIDENT "Auto"; "with"; "*" -> <:ast< (Auto "*") >>
+ | IDENT "Auto"; "with"; "*" -> <:ast< (Auto "*") >>
- | LIDENT "AutoTDB"; n = numarg -> <:ast< (AutoTDB $n) >>
- | LIDENT "AutoTDB" -> <:ast< (AutoTDB) >>
- | LIDENT "DHyp"; id=identarg -> <:ast< (DHyp $id)>>
- | LIDENT "CDHyp"; id=identarg -> <:ast< (CDHyp $id)>>
- | LIDENT "DConcl" -> <:ast< (DConcl)>>
- | LIDENT "SuperAuto";
+ | IDENT "AutoTDB"; n = numarg -> <:ast< (AutoTDB $n) >>
+ | IDENT "AutoTDB" -> <:ast< (AutoTDB) >>
+ | IDENT "DHyp"; id=identarg -> <:ast< (DHyp $id)>>
+ | IDENT "CDHyp"; id=identarg -> <:ast< (CDHyp $id)>>
+ | IDENT "DConcl" -> <:ast< (DConcl)>>
+ | IDENT "SuperAuto";
a0 = autoarg_depth;
a1 = autoarg_adding;
a2 = autoarg_destructing;
a3 = autoarg_usingTDB ->
<:ast< (SuperAuto $a0 $a1 $a2 $a3) >>
- | LIDENT "Auto"; n = numarg; LIDENT "Decomp" -> <:ast< (DAuto $n) >>
- | LIDENT "Auto"; LIDENT "Decomp" -> <:ast< (DAuto) >>
- | LIDENT "Auto"; n = numarg; LIDENT "Decomp"; p = numarg-> <:ast< (DAuto $n $p) >>
+ | IDENT "Auto"; n = numarg; IDENT "Decomp" -> <:ast< (DAuto $n) >>
+ | IDENT "Auto"; IDENT "Decomp" -> <:ast< (DAuto) >>
+ | IDENT "Auto"; n = numarg; IDENT "Decomp"; p = numarg-> <:ast< (DAuto $n $p) >>
]];
END
GEXTEND Gram
simple_tactic:
- [ [ LIDENT "Intros" -> <:ast< (Intros) >>
- | LIDENT "Intros"; LIDENT "until"; id = identarg
+ [ [ IDENT "Intros" -> <:ast< (Intros) >>
+ | IDENT "Intros"; IDENT "until"; id = identarg
-> <:ast< (IntrosUntil $id) >>
- | LIDENT "Intros"; LIDENT "until"; n = numarg -> <:ast<(IntrosUntil $n)>>
- | LIDENT "Intros"; pl = one_intropattern -> <:ast< (Intros $pl) >>
- | LIDENT "Intro"; id = identarg;
- LIDENT "after"; id2 = identarg -> <:ast< (IntroMove $id $id2) >>
- | LIDENT "Intro";
- LIDENT "after"; id2 = identarg -> <:ast< (IntroMove $id2) >>
- | LIDENT "Intro"; id = identarg -> <:ast< (Intro $id) >>
- | LIDENT "Intro" -> <:ast< (Intro) >>
- | LIDENT "Apply"; cl = comarg_binding_list ->
+ | IDENT "Intros"; IDENT "until"; n = numarg -> <:ast<(IntrosUntil $n)>>
+ | IDENT "Intros"; pl = one_intropattern -> <:ast< (Intros $pl) >>
+ | IDENT "Intro"; id = identarg;
+ IDENT "after"; id2 = identarg -> <:ast< (IntroMove $id $id2) >>
+ | IDENT "Intro";
+ IDENT "after"; id2 = identarg -> <:ast< (IntroMove $id2) >>
+ | IDENT "Intro"; id = identarg -> <:ast< (Intro $id) >>
+ | IDENT "Intro" -> <:ast< (Intro) >>
+ | IDENT "Apply"; cl = comarg_binding_list ->
<:ast< (Apply ($LIST $cl)) >>
- | LIDENT "Elim"; cl = comarg_binding_list; "using";
+ | IDENT "Elim"; cl = comarg_binding_list; "using";
el = comarg_binding_list ->
<:ast< (Elim ($LIST $cl) ($LIST $el)) >>
- | LIDENT "Elim"; cl = comarg_binding_list ->
+ | IDENT "Elim"; cl = comarg_binding_list ->
<:ast< (Elim ($LIST $cl)) >>
- | LIDENT "Assumption" -> <:ast< (Assumption) >>
- | LIDENT "Contradiction" -> <:ast< (Contradiction) >>
- | LIDENT "Exact"; c = comarg -> <:ast< (Exact $c) >>
- | LIDENT "OldElim"; c = comarg -> <:ast< (OldElim $c) >>
- | LIDENT "ElimType"; c = comarg -> <:ast< (ElimType $c) >>
- | LIDENT "Case"; cl = comarg_binding_list ->
+ | IDENT "Assumption" -> <:ast< (Assumption) >>
+ | IDENT "Contradiction" -> <:ast< (Contradiction) >>
+ | IDENT "Exact"; c = comarg -> <:ast< (Exact $c) >>
+ | IDENT "OldElim"; c = comarg -> <:ast< (OldElim $c) >>
+ | IDENT "ElimType"; c = comarg -> <:ast< (ElimType $c) >>
+ | IDENT "Case"; cl = comarg_binding_list ->
<:ast< (Case ($LIST $cl)) >>
- | LIDENT "CaseType"; c = comarg -> <:ast< (CaseType $c) >>
- | LIDENT "Destruct"; s = identarg -> <:ast< (Destruct $s) >>
- | LIDENT "Destruct"; n = numarg -> <:ast< (Destruct $n) >>
- | LIDENT "Decompose"; LIDENT "Record" ; c = comarg ->
+ | IDENT "CaseType"; c = comarg -> <:ast< (CaseType $c) >>
+ | IDENT "Destruct"; s = identarg -> <:ast< (Destruct $s) >>
+ | IDENT "Destruct"; n = numarg -> <:ast< (Destruct $n) >>
+ | IDENT "Decompose"; IDENT "Record" ; c = comarg ->
<:ast< (DecomposeAnd $c) >>
- | LIDENT "Decompose"; LIDENT "Sum"; c = comarg ->
+ | IDENT "Decompose"; IDENT "Sum"; c = comarg ->
<:ast< (DecomposeOr $c) >>
- | LIDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = comarg ->
+ | IDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = comarg ->
<:ast< (DecomposeThese (CLAUSE ($LIST $l)) $c) >>
- | LIDENT "First" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
+ | IDENT "First" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
<:ast<(FIRST ($LIST $l))>>
- | LIDENT "Solve" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
+ | IDENT "Solve" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
<:ast<(TCLSOLVE ($LIST $l))>>
- | LIDENT "Cut"; c = comarg -> <:ast< (Cut $c) >>
- | LIDENT "Specialize"; n = numarg; lcb = comarg_binding_list ->
+ | IDENT "Cut"; c = comarg -> <:ast< (Cut $c) >>
+ | IDENT "Specialize"; n = numarg; lcb = comarg_binding_list ->
<:ast< (Specialize $n ($LIST $lcb))>>
- | LIDENT "Specialize"; lcb = comarg_binding_list ->
+ | IDENT "Specialize"; lcb = comarg_binding_list ->
<:ast< (Specialize ($LIST $lcb)) >>
- | LIDENT "Generalize"; lc = comarg_list ->
+ | IDENT "Generalize"; lc = comarg_list ->
<:ast< (Generalize ($LIST $lc)) >>
- | LIDENT "Generalize"; LIDENT "Dependent"; c = comarg ->
+ | IDENT "Generalize"; IDENT "Dependent"; c = comarg ->
<:ast< (GeneralizeDep $c) >>
- | LIDENT "Let"; s = identarg; ":="; c = comarg; "in";
+ | IDENT "Let"; s = identarg; ":="; c = comarg; "in";
l = ne_pattern_hyp_list ->
<:ast< (LetTac $s $c (LETPATTERNS ($LIST $l))) >>
- | LIDENT "LApply"; c = comarg -> <:ast< (CutAndApply $c) >>
- | LIDENT "Clear"; l = ne_identarg_list ->
+ | IDENT "LApply"; c = comarg -> <:ast< (CutAndApply $c) >>
+ | IDENT "Clear"; l = ne_identarg_list ->
<:ast< (Clear (CLAUSE ($LIST $l))) >>
- | LIDENT "Move"; id1 = identarg; LIDENT "after"; id2 = identarg ->
+ | IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg ->
<:ast< (MoveDep $id1 $id2) >>
- | LIDENT "Do"; n = numarg; tc = tactic_com -> <:ast< (DO $n $tc) >>
- | LIDENT "Try"; tc = tactic_com -> <:ast< (TRY $tc) >>
- | LIDENT "Info"; tc = tactic_com -> <:ast< (INFO $tc) >>
- | LIDENT "Repeat"; tc = tactic_com -> <:ast< (REPEAT $tc) >>
- | LIDENT "Abstract"; tc = tactic_com -> <:ast< (ABSTRACT (TACTIC $tc)) >>
- | LIDENT "Abstract"; tc = tactic_com; "using"; s=identarg
+ | IDENT "Do"; n = numarg; tc = tactic_com -> <:ast< (DO $n $tc) >>
+ | IDENT "Try"; tc = tactic_com -> <:ast< (TRY $tc) >>
+ | IDENT "Info"; tc = tactic_com -> <:ast< (INFO $tc) >>
+ | IDENT "Repeat"; tc = tactic_com -> <:ast< (REPEAT $tc) >>
+ | IDENT "Abstract"; tc = tactic_com -> <:ast< (ABSTRACT (TACTIC $tc)) >>
+ | IDENT "Abstract"; tc = tactic_com; "using"; s=identarg
-> <:ast< (ABSTRACT $s (TACTIC $tc)) >>
- | LIDENT "Left"; bl = with_binding_list -> <:ast< (Left $bl) >>
- | LIDENT "Right"; bl = with_binding_list -> <:ast< (Right $bl) >>
- | LIDENT "Split"; bl = with_binding_list -> <:ast< (Split $bl) >>
- | LIDENT "Exists"; bl = binding_list -> <:ast< (Split $bl) >>
- | LIDENT "Constructor"; nbl = numarg_binding_list ->
+ | IDENT "Left"; bl = with_binding_list -> <:ast< (Left $bl) >>
+ | IDENT "Right"; bl = with_binding_list -> <:ast< (Right $bl) >>
+ | IDENT "Split"; bl = with_binding_list -> <:ast< (Split $bl) >>
+ | IDENT "Exists"; bl = binding_list -> <:ast< (Split $bl) >>
+ | IDENT "Constructor"; nbl = numarg_binding_list ->
<:ast<(Constructor ($LIST $nbl)) >>
- | LIDENT "Constructor" -> <:ast<(Constructor) >>
- | LIDENT "Reflexivity" -> <:ast< (Reflexivity) >>
- | LIDENT "Symmetry" -> <:ast< (Symmetry) >>
- | LIDENT "Transitivity"; c = comarg -> <:ast< (Transitivity $c) >>
- | LIDENT "Absurd"; c = comarg -> <:ast< (Absurd $c) >>
- | LIDENT "Idtac" -> <:ast< (Idtac) >>
- | LIDENT "Fail" -> <:ast< (Fail) >>
+ | IDENT "Constructor" -> <:ast<(Constructor) >>
+ | IDENT "Reflexivity" -> <:ast< (Reflexivity) >>
+ | IDENT "Symmetry" -> <:ast< (Symmetry) >>
+ | IDENT "Transitivity"; c = comarg -> <:ast< (Transitivity $c) >>
+ | IDENT "Absurd"; c = comarg -> <:ast< (Absurd $c) >>
+ | IDENT "Idtac" -> <:ast< (Idtac) >>
+ | IDENT "Fail" -> <:ast< (Fail) >>
| "("; tcl = tactic_com_list; ")" -> tcl
| r = red_tactic; cl = clausearg -> <:ast< (Reduce (REDEXP $r) $cl) >> ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 740498fad1..5d2679407e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -7,7 +7,7 @@ open Tactic
GEXTEND Gram
simple_tactic:
- [ [ LIDENT "ML"; s = Prim.string -> <:ast< (MLTACTIC $s) >> ] ]
+ [ [ IDENT "ML"; s = Prim.string -> <:ast< (MLTACTIC $s) >> ] ]
;
END
@@ -38,8 +38,8 @@ GEXTEND Gram
<:ast< (VERNACARGLIST ($LIST $l)) >> ] ]
;
destruct_location :
- [ [ LIDENT "Conclusion" -> <:ast< (CONCL)>>
- | LIDENT "Discardable"; "Hypothesis" -> <:ast< (DiscardableHYP)>>
+ [ [ IDENT "Conclusion" -> <:ast< (CONCL)>>
+ | IDENT "Discardable"; "Hypothesis" -> <:ast< (DiscardableHYP)>>
| "Hypothesis" -> <:ast< (PreciousHYP)>> ]]
;
ne_comarg_list:
@@ -93,8 +93,8 @@ GEXTEND Gram
| -> <:ast< (VERNACARGLIST) >> ] ]
;
record_tok:
- [ [ LIDENT "Record" -> <:ast< "Record" >>
- | LIDENT "Structure" -> <:ast< "Structure" >> ] ]
+ [ [ IDENT "Record" -> <:ast< "Record" >>
+ | IDENT "Structure" -> <:ast< "Structure" >> ] ]
;
field:
[ [ id = identarg; ":"; c = Command.command ->
@@ -111,7 +111,7 @@ GEXTEND Gram
| -> <:ast< (VERNACARGLIST) >> ] ]
;
onescheme:
- [ [ id = identarg; ":="; dep = dep; c = comarg; LIDENT "Sort";
+ [ [ id = identarg; ":="; dep = dep; c = comarg; IDENT "Sort";
s = sortdef ->
<:ast< (VERNACARGLIST $id $dep $c (COMMAND $s)) >> ] ]
;
@@ -120,8 +120,8 @@ GEXTEND Gram
| rec_ = onescheme -> [rec_] ] ]
;
dep:
- [ [ LIDENT "Induction"; LIDENT "for" -> <:ast< "DEP" >>
- | LIDENT "Minimality"; LIDENT "for" -> <:ast< "NODEP" >> ] ]
+ [ [ IDENT "Induction"; IDENT "for" -> <:ast< "DEP" >>
+ | IDENT "Minimality"; IDENT "for" -> <:ast< "NODEP" >> ] ]
;
ne_binder_semi_list:
[ [ id = binder; ";"; idl = ne_binder_semi_list -> id :: idl
@@ -139,29 +139,29 @@ GEXTEND Gram
;
thm_tok:
[ [ "Theorem" -> <:ast< "THEOREM" >>
- | LIDENT "Lemma" -> <:ast< "LEMMA" >>
- | LIDENT "Fact" -> <:ast< "FACT" >>
- | LIDENT "Remark" -> <:ast< "REMARK" >> ] ]
+ | IDENT "Lemma" -> <:ast< "LEMMA" >>
+ | IDENT "Fact" -> <:ast< "FACT" >>
+ | IDENT "Remark" -> <:ast< "REMARK" >> ] ]
;
def_tok:
[ [ "Definition" -> <:ast< "DEFINITION" >>
- | LIDENT "Local" -> <:ast< "LOCAL" >>
+ | IDENT "Local" -> <:ast< "LOCAL" >>
| "@"; "Definition" -> <:ast< "OBJECT" >>
- | "@"; LIDENT "Local" -> <:ast< "LOBJECT" >>
- | "@"; LIDENT "Coercion" -> <:ast< "OBJCOERCION" >>
- | "@"; LIDENT "Local"; LIDENT "Coercion" -> <:ast< "LOBJCOERCION" >>
- | LIDENT "SubClass" -> <:ast< "SUBCLASS" >>
- | LIDENT "Local"; LIDENT "SubClass" -> <:ast< "LSUBCLASS" >> ] ]
+ | "@"; IDENT "Local" -> <:ast< "LOBJECT" >>
+ | "@"; IDENT "Coercion" -> <:ast< "OBJCOERCION" >>
+ | "@"; IDENT "Local"; IDENT "Coercion" -> <:ast< "LOBJCOERCION" >>
+ | IDENT "SubClass" -> <:ast< "SUBCLASS" >>
+ | IDENT "Local"; IDENT "SubClass" -> <:ast< "LSUBCLASS" >> ] ]
;
import_tok:
- [ [ LIDENT "Import" -> <:ast< "IMPORT" >>
- | LIDENT "Export" -> <:ast< "EXPORT" >>
+ [ [ IDENT "Import" -> <:ast< "IMPORT" >>
+ | IDENT "Export" -> <:ast< "EXPORT" >>
| -> <:ast< "IMPORT" >> ] ]
;
specif_tok:
- [ [ LIDENT "Implementation" -> <:ast< "IMPLEMENTATION" >>
- | LIDENT "Specification" -> <:ast< "SPECIFICATION" >>
+ [ [ IDENT "Implementation" -> <:ast< "IMPLEMENTATION" >>
+ | IDENT "Specification" -> <:ast< "SPECIFICATION" >>
| -> <:ast< "UNSPECIFIED" >> ] ]
;
hyp_tok:
@@ -169,22 +169,22 @@ GEXTEND Gram
| "Variable" -> <:ast< "VARIABLE" >> ] ]
;
hyps_tok:
- [ [ LIDENT "Hypotheses" -> <:ast< "HYPOTHESES" >>
- | LIDENT "Variables" -> <:ast< "VARIABLES" >> ] ]
+ [ [ IDENT "Hypotheses" -> <:ast< "HYPOTHESES" >>
+ | IDENT "Variables" -> <:ast< "VARIABLES" >> ] ]
;
param_tok:
[ [ "Axiom" -> <:ast< "AXIOM" >>
| "Parameter" -> <:ast< "PARAMETER" >> ] ]
;
params_tok:
- [ [ LIDENT "Parameters" -> <:ast< "PARAMETERS" >> ] ]
+ [ [ IDENT "Parameters" -> <:ast< "PARAMETERS" >> ] ]
;
binder:
[ [ idl = ne_identarg_comma_list; ":"; c = Command.command ->
<:ast< (BINDER $c ($LIST $idl)) >> ] ]
;
idcom:
- [ [ id = LIDENT; ":"; c = Command.command ->
+ [ [ id = IDENT; ":"; c = Command.command ->
<:ast< (BINDER $c ($VAR $id)) >> ] ]
;
ne_lidcom:
@@ -225,15 +225,15 @@ GEXTEND Gram
*)
| def = def_tok; s = identarg; ":=";
- LIDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Command.command; "." ->
+ IDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Command.command; "." ->
<:ast< (DEFINITION $def $s (COMMAND $c1) (TACTIC_ARG (REDEXP $r))) >>
| def = def_tok; s = identarg; ":=";
- LIDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Command.command; ":";
+ IDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Command.command; ":";
c2 = Command.command; "." ->
<:ast< (DEFINITION $def $s
(COMMAND (CAST $c1 $c2)) (TACTIC_ARG (REDEXP $r))) >>
| def = def_tok; s = identarg; ":"; c1 = Command.command; ":=";
- LIDENT "Eval"; r = Tactic.red_tactic; "in";
+ IDENT "Eval"; r = Tactic.red_tactic; "in";
c2 = Command.command; "." ->
<:ast< (DEFINITION $def $s (COMMAND (CAST $c2 $c1))
(TACTIC_ARG (REDEXP $r))) >>
@@ -242,11 +242,11 @@ GEXTEND Gram
Ajout du racourci "Definition x [c:nat] := t" pour
"Definition x := [c:nat]t" *)
- | def = def_tok; s = identarg; "["; id1 = LIDENT; ":";
+ | def = def_tok; s = identarg; "["; id1 = IDENT; ":";
c = Command.command; t = definition_tail; "." ->
<:ast< (DEFINITION $def $s (COMMAND (LAMBDA $c [$id1]$t))) >>
- | def = def_tok; s = identarg; "["; id1 = LIDENT; ",";
+ | def = def_tok; s = identarg; "["; id1 = IDENT; ",";
idl = Command.ne_ident_comma_list; ":"; c = Command.command;
t = definition_tail; "." ->
<:ast< (DEFINITION $def $s (COMMAND
@@ -261,7 +261,7 @@ GEXTEND Gram
<:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
| hyp = params_tok; bl = ne_binder_semi_list; "." ->
<:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
- | LIDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]";
+ | IDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]";
":="; c = comarg; "." ->
<:ast< (ABSTRACTION $id $c ($LIST $l)) >>
| f = finite_tok; "Set"; id = identarg; indpar = indpar; ":=";
@@ -285,17 +285,17 @@ GEXTEND Gram
c = rec_constr; "{"; fs = fields; "}"; "." ->
<:ast< (RECORD "COERCION" $name $ps (COMMAND $s) $c $fs) >>
- | LIDENT "Mutual"; "["; bl = ne_binder_semi_list; "]" ; f = finite_tok;
+ | IDENT "Mutual"; "["; bl = ne_binder_semi_list; "]" ; f = finite_tok;
indl = block_old_style; "." ->
<:ast< (OLDMUTUALINDUCTIVE (BINDERLIST ($LIST $bl)) $f
(VERNACARGLIST ($LIST $indl))) >>
- | LIDENT "Mutual"; f = finite_tok; indl = block; "." ->
+ | IDENT "Mutual"; f = finite_tok; indl = block; "." ->
<:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >>
| "Fixpoint"; recs = specifrec; "." ->
<:ast< (MUTUALRECURSIVE (VERNACARGLIST ($LIST $recs))) >>
| "CoFixpoint"; corecs = specifcorec; "." ->
<:ast< (MUTUALCORECURSIVE (VERNACARGLIST ($LIST $corecs))) >>
- | LIDENT "Scheme"; schemes = specifscheme; "." ->
+ | IDENT "Scheme"; schemes = specifscheme; "." ->
<:ast< (INDUCTIONSCHEME (VERNACARGLIST ($LIST $schemes))) >>
] ];
@@ -315,96 +315,96 @@ GEXTEND Gram
GEXTEND Gram
vernac:
[ [
- LIDENT "Save"; LIDENT "State"; id = identarg; "." ->
+ IDENT "Save"; IDENT "State"; id = identarg; "." ->
<:ast< (SaveState $id "") >>
- | LIDENT "Save"; LIDENT "State"; id = identarg; s = stringarg; "." ->
+ | IDENT "Save"; IDENT "State"; id = identarg; s = stringarg; "." ->
<:ast< (SaveState $id $s) >>
- | LIDENT "Write"; LIDENT "States"; id = identarg; "." ->
+ | IDENT "Write"; IDENT "States"; id = identarg; "." ->
<:ast< (WriteStates $id) >>
- | LIDENT "Write"; LIDENT "States"; id = stringarg; "." ->
+ | IDENT "Write"; IDENT "States"; id = stringarg; "." ->
<:ast< (WriteStates $id) >>
- | LIDENT "Restore"; LIDENT "State"; id = identarg; "." ->
+ | IDENT "Restore"; IDENT "State"; id = identarg; "." ->
<:ast< (RestoreState $id) >>
- | LIDENT "Remove"; LIDENT "State"; id = identarg; "." ->
+ | IDENT "Remove"; IDENT "State"; id = identarg; "." ->
<:ast< (RemoveState $id) >>
- | LIDENT "Reset"; LIDENT "after"; id = identarg; "." ->
+ | IDENT "Reset"; IDENT "after"; id = identarg; "." ->
<:ast< (ResetAfter $id) >>
- | LIDENT "Reset"; LIDENT "Initial"; "." -> <:ast< (ResetInitial) >>
- | LIDENT "Reset"; LIDENT "Section"; id = identarg; "." ->
+ | IDENT "Reset"; IDENT "Initial"; "." -> <:ast< (ResetInitial) >>
+ | IDENT "Reset"; IDENT "Section"; id = identarg; "." ->
<:ast< (ResetSection $id) >>
- | LIDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >>
+ | IDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >>
(* Modules and Sections *)
- | LIDENT "Read"; LIDENT "Module"; id = identarg; "." ->
+ | IDENT "Read"; IDENT "Module"; id = identarg; "." ->
<:ast< (ReadModule $id) >>
- | LIDENT "Require"; import = import_tok; specif = specif_tok;
+ | IDENT "Require"; import = import_tok; specif = specif_tok;
id = identarg; "." -> <:ast< (Require $import $specif $id) >>
- | LIDENT "Require"; import = import_tok; specif = specif_tok;
+ | IDENT "Require"; import = import_tok; specif = specif_tok;
id = identarg; filename = stringarg; "." ->
<:ast< (RequireFrom $import $specif $id $filename) >>
- | LIDENT "Section"; id = identarg; "." -> <:ast< (BeginSection $id) >>
- | LIDENT "Chapter"; id = identarg; "." -> <:ast< (BeginSection $id) >>
- | LIDENT "Module"; id = identarg; "." -> <:ast< (BeginModule $id) >>
- | LIDENT "Begin"; LIDENT "Silent"; "." -> <:ast< (BeginSilent) >>
- | LIDENT "End"; LIDENT "Silent"; "." -> <:ast< (EndSilent) >>
- | LIDENT "End"; id = identarg; "." -> <:ast< (EndSection $id) >>
- | LIDENT "Declare"; LIDENT "ML"; LIDENT "Module";
+ | IDENT "Section"; id = identarg; "." -> <:ast< (BeginSection $id) >>
+ | IDENT "Chapter"; id = identarg; "." -> <:ast< (BeginSection $id) >>
+ | IDENT "Module"; id = identarg; "." -> <:ast< (BeginModule $id) >>
+ | IDENT "Begin"; IDENT "Silent"; "." -> <:ast< (BeginSilent) >>
+ | IDENT "End"; IDENT "Silent"; "." -> <:ast< (EndSilent) >>
+ | IDENT "End"; id = identarg; "." -> <:ast< (EndSection $id) >>
+ | IDENT "Declare"; IDENT "ML"; IDENT "Module";
l = ne_stringarg_list; "." -> <:ast< (DeclareMLModule ($LIST $l)) >>
- | LIDENT "Import"; id = identarg; "." -> <:ast< (ImportModule $id) >>
+ | IDENT "Import"; id = identarg; "." -> <:ast< (ImportModule $id) >>
(* Transparent and Opaque *)
- | LIDENT "Transparent"; l = ne_identarg_list; "." ->
+ | IDENT "Transparent"; l = ne_identarg_list; "." ->
<:ast< (TRANSPARENT ($LIST $l)) >>
- | LIDENT "Opaque"; l = ne_identarg_list; "." ->
+ | IDENT "Opaque"; l = ne_identarg_list; "." ->
<:ast< (OPAQUE ($LIST $l)) >>
(* Extraction *)
- | LIDENT "Extraction"; id = identarg; "." ->
+ | IDENT "Extraction"; id = identarg; "." ->
<:ast< (PrintExtractId $id) >>
- | LIDENT "Extraction"; "." -> <:ast< (PrintExtract) >>
+ | IDENT "Extraction"; "." -> <:ast< (PrintExtract) >>
(* Grammar extensions, Coercions, Implicits *)
- | LIDENT "Coercion"; s = identarg; ":="; c1 = Command.command; "." ->
+ | IDENT "Coercion"; s = identarg; ":="; c1 = Command.command; "." ->
<:ast< (DEFINITION "COERCION" $s (COMMAND $c1)) >>
- | LIDENT "Coercion"; s = identarg; ":="; c1 = Command.command; ":";
+ | IDENT "Coercion"; s = identarg; ":="; c1 = Command.command; ":";
c2 = Command.command; "." ->
<:ast< (DEFINITION "COERCION" $s (COMMAND (CAST $c1 $c2))) >>
- | LIDENT "Coercion"; LIDENT "Local"; s = identarg; ":=";
+ | IDENT "Coercion"; IDENT "Local"; s = identarg; ":=";
c1 = Command.command; "." ->
<:ast< (DEFINITION "LCOERCION" $s (COMMAND $c1)) >>
- | LIDENT "Coercion"; LIDENT "Local"; s = identarg; ":=";
+ | IDENT "Coercion"; IDENT "Local"; s = identarg; ":=";
c1 = Command.command; ":"; c2 = Command.command; "." ->
<:ast< (DEFINITION "LCOERCION" $s (COMMAND (CAST $c1 $c2))) >>
- | LIDENT "Syntactic"; "Definition"; id = identarg; ":="; com = comarg;
+ | IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = comarg;
"." -> <:ast< (SyntaxMacro $id $com) >>
- | LIDENT "Syntactic"; "Definition"; id = identarg; ":="; com = comarg;
+ | IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = comarg;
"|"; n = numarg; "." -> <:ast< (SyntaxMacro $id $com $n) >>
- | LIDENT "Print"; "Grammar"; uni = identarg; ent = identarg; "." ->
+ | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg; "." ->
<:ast< (PrintGrammar $uni $ent) >>
- | LIDENT "Identity"; LIDENT "Coercion"; LIDENT "Local"; f = identarg;
+ | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identarg;
":"; c = identarg; ">->"; d = identarg; "." ->
<:ast< (COERCION "LOCAL" "IDENTITY" $f $c $d) >>
- | LIDENT "Identity"; LIDENT "Coercion"; f = identarg; ":";
+ | IDENT "Identity"; IDENT "Coercion"; f = identarg; ":";
c = identarg; ">->"; d = identarg; "." ->
<:ast< (COERCION "" "IDENTITY" $f $c $d) >>
- | LIDENT "Coercion"; LIDENT "Local"; f = identarg; ":"; c = identarg;
+ | IDENT "Coercion"; IDENT "Local"; f = identarg; ":"; c = identarg;
">->"; d = identarg; "." ->
<:ast< (COERCION "LOCAL" "" $f $c $d) >>
- | LIDENT "Coercion"; f = identarg; ":"; c = identarg; ">->";
+ | IDENT "Coercion"; f = identarg; ":"; c = identarg; ">->";
d = identarg; "." -> <:ast< (COERCION "" "" $f $c $d) >>
- | LIDENT "Class"; LIDENT "Local"; c = identarg; "." ->
+ | IDENT "Class"; IDENT "Local"; c = identarg; "." ->
<:ast< (CLASS "LOCAL" $c) >>
- | LIDENT "Class"; c = identarg; "." -> <:ast< (CLASS "" $c) >>
- | LIDENT "Implicit"; LIDENT "Arguments"; LIDENT "On"; "." ->
+ | IDENT "Class"; c = identarg; "." -> <:ast< (CLASS "" $c) >>
+ | IDENT "Implicit"; IDENT "Arguments"; IDENT "On"; "." ->
<:ast< (IMPLICIT_ARGS_ON) >>
- | LIDENT "Implicit"; LIDENT "Arguments"; LIDENT "Off"; "." ->
+ | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off"; "." ->
<:ast< (IMPLICIT_ARGS_OFF) >>
- | LIDENT "Implicits"; id = identarg; "["; l = numarg_list; "]"; "." ->
+ | IDENT "Implicits"; id = identarg; "["; l = numarg_list; "]"; "." ->
<:ast< (IMPLICITS "" $id ($LIST $l)) >>
- | LIDENT "Implicits"; id = identarg; "." ->
+ | IDENT "Implicits"; id = identarg; "." ->
<:ast< (IMPLICITS "Auto" $id) >>
] ];
END
@@ -412,103 +412,103 @@ GEXTEND Gram
(* Proof commands *)
GEXTEND Gram
vernac:
- [ [ LIDENT "Goal"; c = comarg; "." -> <:ast< (GOAL $c) >>
- | LIDENT "Goal"; "." -> <:ast< (GOAL) >>
+ [ [ IDENT "Goal"; c = comarg; "." -> <:ast< (GOAL $c) >>
+ | IDENT "Goal"; "." -> <:ast< (GOAL) >>
| "Proof"; "." -> <:ast< (GOAL) >>
- | LIDENT "Abort"; "." -> <:ast< (ABORT) >>
+ | IDENT "Abort"; "." -> <:ast< (ABORT) >>
| "Qed"; "." -> <:ast< (SaveNamed) >>
- | LIDENT "Save"; "." -> <:ast< (SaveNamed) >>
- | LIDENT "Defined"; "." -> <:ast< (DefinedNamed) >>
- | LIDENT "Save"; LIDENT "Remark"; id = identarg; "." ->
+ | IDENT "Save"; "." -> <:ast< (SaveNamed) >>
+ | IDENT "Defined"; "." -> <:ast< (DefinedNamed) >>
+ | IDENT "Save"; IDENT "Remark"; id = identarg; "." ->
<:ast< (SaveAnonymousRmk $id) >>
- | LIDENT "Save"; LIDENT "Theorem"; id = identarg; "." ->
+ | IDENT "Save"; IDENT "Theorem"; id = identarg; "." ->
<:ast< (SaveAnonymousThm $id) >>
- | LIDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymousThm $id) >>
- | LIDENT "Suspend"; "." -> <:ast< (SUSPEND) >>
- | LIDENT "Resume"; "." -> <:ast< (RESUME) >>
- | LIDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >>
- | LIDENT "Abort"; LIDENT "All"; "." -> <:ast< (ABORTALL) >>
- | LIDENT "Abort"; id = identarg; "." -> <:ast< (ABORT $id) >>
- | LIDENT "Restart"; "." -> <:ast< (RESTART) >>
+ | IDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymousThm $id) >>
+ | IDENT "Suspend"; "." -> <:ast< (SUSPEND) >>
+ | IDENT "Resume"; "." -> <:ast< (RESUME) >>
+ | IDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >>
+ | IDENT "Abort"; IDENT "All"; "." -> <:ast< (ABORTALL) >>
+ | IDENT "Abort"; id = identarg; "." -> <:ast< (ABORT $id) >>
+ | IDENT "Restart"; "." -> <:ast< (RESTART) >>
| "Proof"; c = comarg; "." -> <:ast< (PROOF $c) >>
- | LIDENT "Undo"; "." -> <:ast< (UNDO 1) >>
- | LIDENT "Undo"; n = numarg; "." -> <:ast< (UNDO $n) >>
- | LIDENT "Show"; n = numarg; "." -> <:ast< (SHOW $n) >>
- | LIDENT "Show"; LIDENT "Implicits"; n = numarg; "." ->
+ | IDENT "Undo"; "." -> <:ast< (UNDO 1) >>
+ | IDENT "Undo"; n = numarg; "." -> <:ast< (UNDO $n) >>
+ | IDENT "Show"; n = numarg; "." -> <:ast< (SHOW $n) >>
+ | IDENT "Show"; IDENT "Implicits"; n = numarg; "." ->
<:ast< (SHOWIMPL $n) >>
- | LIDENT "Focus"; "." -> <:ast< (FOCUS) >>
- | LIDENT "Focus"; n = numarg; "." -> <:ast< (FOCUS $n) >>
- | LIDENT "Unfocus"; "." -> <:ast< (UNFOCUS) >>
- | LIDENT "Show"; "." -> <:ast< (SHOW) >>
- | LIDENT "Show"; LIDENT "Implicits"; "." -> <:ast< (SHOWIMPL) >>
- | LIDENT "Show"; LIDENT "Node"; "." -> <:ast< (ShowNode) >>
- | LIDENT "Show"; LIDENT "Script"; "." -> <:ast< (ShowScript) >>
- | LIDENT "Show"; LIDENT "Existentials"; "." -> <:ast< (ShowEx) >>
- | LIDENT "Existential"; n = numarg; ":="; c = Command.command; "." ->
+ | IDENT "Focus"; "." -> <:ast< (FOCUS) >>
+ | IDENT "Focus"; n = numarg; "." -> <:ast< (FOCUS $n) >>
+ | IDENT "Unfocus"; "." -> <:ast< (UNFOCUS) >>
+ | IDENT "Show"; "." -> <:ast< (SHOW) >>
+ | IDENT "Show"; IDENT "Implicits"; "." -> <:ast< (SHOWIMPL) >>
+ | IDENT "Show"; IDENT "Node"; "." -> <:ast< (ShowNode) >>
+ | IDENT "Show"; IDENT "Script"; "." -> <:ast< (ShowScript) >>
+ | IDENT "Show"; IDENT "Existentials"; "." -> <:ast< (ShowEx) >>
+ | IDENT "Existential"; n = numarg; ":="; c = Command.command; "." ->
<:ast< (EXISTENTIAL $n (COMMAND $c)) >>
- | LIDENT "Existential"; n = numarg; ":="; c1 = Command.command; ":";
+ | IDENT "Existential"; n = numarg; ":="; c1 = Command.command; ":";
c2 = Command.command; "." ->
<:ast< (EXISTENTIAL $n (COMMAND (CAST $c1 $c2))) >>
- | LIDENT "Existential"; n = numarg; ":"; c2 = Command.command; ":=";
+ | IDENT "Existential"; n = numarg; ":"; c2 = Command.command; ":=";
c1 = Command.command; "." ->
<:ast< (EXISTENTIAL $n (COMMAND (CAST $c1 $c2))) >>
- | LIDENT "Explain"; "Proof"; l = numarg_list; "." ->
+ | IDENT "Explain"; "Proof"; l = numarg_list; "." ->
<:ast< (ExplainProof ($LIST $l)) >>
- | LIDENT "Explain"; "Proof"; LIDENT "Tree"; l = numarg_list; "." ->
+ | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list; "." ->
<:ast< (ExplainProofTree ($LIST $l)) >>
- | LIDENT "Go"; n = numarg; "." -> <:ast< (Go $n) >>
- | LIDENT "Go"; LIDENT "top"; "." -> <:ast< (Go "top") >>
- | LIDENT "Go"; LIDENT "prev"; "." -> <:ast< (Go "prev") >>
- | LIDENT "Go"; LIDENT "next"; "." -> <:ast< (Go "next") >>
- | LIDENT "Show"; "Proof"; "." -> <:ast< (ShowProof) >>
- | LIDENT "Guarded"; "." -> <:ast< (CheckGuard) >>
- | LIDENT "Show"; LIDENT "Tree"; "." -> <:ast< (ShowTree) >>
- | LIDENT "Show"; LIDENT "Conjectures"; "." -> <:ast< (ShowProofs) >>
+ | IDENT "Go"; n = numarg; "." -> <:ast< (Go $n) >>
+ | IDENT "Go"; IDENT "top"; "." -> <:ast< (Go "top") >>
+ | IDENT "Go"; IDENT "prev"; "." -> <:ast< (Go "prev") >>
+ | IDENT "Go"; IDENT "next"; "." -> <:ast< (Go "next") >>
+ | IDENT "Show"; "Proof"; "." -> <:ast< (ShowProof) >>
+ | IDENT "Guarded"; "." -> <:ast< (CheckGuard) >>
+ | IDENT "Show"; IDENT "Tree"; "." -> <:ast< (ShowTree) >>
+ | IDENT "Show"; IDENT "Conjectures"; "." -> <:ast< (ShowProofs) >>
(* Tactic Definition *)
- | LIDENT "Tactic"; "Definition"; id = identarg; "[";
+ | IDENT "Tactic"; "Definition"; id = identarg; "[";
ids = ne_identarg_list; "]"; ":="; tac = Prim.astact; "." ->
<:ast< (TacticDefinition $id (AST $tac) ($LIST $ids)) >>
- | LIDENT "Tactic"; "Definition"; id = identarg; ":="; tac = Prim.astact;
+ | IDENT "Tactic"; "Definition"; id = identarg; ":="; tac = Prim.astact;
"." -> <:ast< (TacticDefinition $id (AST $tac)) >>
(* Hints for Auto and EAuto *)
- | LIDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":=";
- LIDENT "Resolve"; c = comarg; "." ->
+ | IDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":=";
+ IDENT "Resolve"; c = comarg; "." ->
<:ast<(HintResolve $hintname (VERNACARGLIST ($LIST $dbname)) $c)>>
- | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- LIDENT "Immediate"; c = comarg; "." ->
+ | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+ IDENT "Immediate"; c = comarg; "." ->
<:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
- | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- LIDENT "Unfold"; c = identarg; "." ->
+ | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+ IDENT "Unfold"; c = identarg; "." ->
<:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
- | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- LIDENT "Constructors"; c = identarg; "." ->
+ | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+ IDENT "Constructors"; c = identarg; "." ->
<:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
- | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- LIDENT "Extern"; n = numarg; c = comarg ; tac = tacarg; "." ->
+ | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+ IDENT "Extern"; n = numarg; c = comarg ; tac = tacarg; "." ->
<:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames))
$n $c (TACTIC $tac))>>
- | LIDENT "Hints"; LIDENT "Resolve"; l = ne_identarg_list;
+ | IDENT "Hints"; IDENT "Resolve"; l = ne_identarg_list;
dbnames = opt_identarg_list; "." ->
<:ast< (HintsResolve (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
- | LIDENT "Hints"; LIDENT "Immediate"; l = ne_identarg_list;
+ | IDENT "Hints"; IDENT "Immediate"; l = ne_identarg_list;
dbnames = opt_identarg_list; "." ->
<:ast< (HintsImmediate (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
- | LIDENT "Hints"; LIDENT "Unfold"; l = ne_identarg_list;
+ | IDENT "Hints"; IDENT "Unfold"; l = ne_identarg_list;
dbnames = opt_identarg_list; "." ->
<:ast< (HintsUnfold (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
- | LIDENT "HintDestruct";
+ | IDENT "HintDestruct";
dloc = destruct_location;
na = identarg;
hyptyp = comarg;
@@ -520,7 +520,7 @@ GEXTEND Gram
<:ast< (SOLVE $n (TACTIC $tac)) >>
(*This entry is not commented, only for debug*)
- | LIDENT "PrintConstr"; com = comarg; "." ->
+ | IDENT "PrintConstr"; com = comarg; "." ->
<:ast< (PrintConstr $com)>>
] ];
END
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 5a2f980f5b..c185a03430 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -60,11 +60,12 @@ let comment_start_pos = ref 0
let blank = [' ' '\010' '\013' '\009' '\012']
let firstchar =
- ['A'-'Z' 'a'-'z' '\192'-'\214' '\216'-'\246' '\248'-'\255']
+ ['$' 'A'-'Z' 'a'-'z' '\192'-'\214' '\216'-'\246' '\248'-'\255']
let identchar =
- ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+ ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255'
+ '\'' '0'-'9']
let symbolchar =
- ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' ':' '=' '?' '@' '^' '|' '~']
+ ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' ':' '=' '?' '@' '^' '|' '~' '#']
let decimal_literal = ['0'-'9']+
let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
let oct_literal = '0' ['o' 'O'] ['0'-'7']+
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 714f29aea2..b1c80bd3e8 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -26,8 +26,8 @@ module L =
let lexer = lexer
end
-
(* The parser of Coq *)
+
module G = Grammar.Make(L)
let grammar_delete e rls =
@@ -40,7 +40,6 @@ type typed_entry =
| Ast of Coqast.t G.Entry.e
| ListAst of Coqast.t list G.Entry.e
-
type ext_kind =
| ByGrammar of
typed_entry * Gramext.position option *
@@ -48,7 +47,6 @@ type ext_kind =
(Gramext.g_symbol list * Gramext.g_action) list) list
| ByGEXTEND of (unit -> unit) * (unit -> unit)
-
let camlp4_state = ref []
(* The apparent parser of Coq; encapsulate G to keep track of the
@@ -74,10 +72,11 @@ module Gram =
(* This extension command is used by the Grammar command *)
+
let grammar_extend te pos rls =
camlp4_state := ByGrammar (te,pos,rls) :: !camlp4_state;
match te with
- Ast e -> G.extend e pos rls
+ | Ast e -> G.extend e pos rls
| ListAst e -> G.extend e pos rls
(* n is the number of extended entries (not the number of Grammar commands!)
@@ -85,7 +84,7 @@ let grammar_extend te pos rls =
let rec remove_grammars n =
if n>0 then
(match !camlp4_state with
- [] -> anomaly "Pcoq.remove_grammars: too many rules to remove"
+ | [] -> anomaly "Pcoq.remove_grammars: too many rules to remove"
| ByGrammar(Ast e,_,rls)::t ->
grammar_delete e rls;
camlp4_state := t;
@@ -101,8 +100,6 @@ let rec remove_grammars n =
redo();
camlp4_state := ByGEXTEND (undo,redo) :: !camlp4_state)
-
-
(* An entry that checks we reached the end of the input. *)
let eoi_entry en =
let e = Gram.Entry.create ((Gram.Entry.name en) ^ "_eoi") in
@@ -120,105 +117,91 @@ let map_entry f en =
END;
e
-
(* Parse a string, does NOT check if the entire string was read
(use eoi_entry) *)
+
let parse_string f x =
let strm = Stream.of_string x in Gram.Entry.parse f (Gram.parsable strm)
-
-
let slam_ast loc id ast =
match id with
- Coqast.Nvar (_, s) -> Coqast.Slam (loc, Some s, ast)
- | _ -> invalid_arg "Ast.slam_ast"
-
+ | Coqast.Nvar (_, s) -> Coqast.Slam (loc, Some s, ast)
+ | _ -> invalid_arg "Ast.slam_ast"
type entry_type = ETast | ETastl
-
+
let entry_type ast =
match ast with
- Coqast.Id (_, "LIST") -> ETastl
- | Coqast.Id (_, "AST") -> ETast
- | _ -> invalid_arg "Ast.entry_type"
-
+ | Coqast.Id (_, "LIST") -> ETastl
+ | Coqast.Id (_, "AST") -> ETast
+ | _ -> invalid_arg "Ast.entry_type"
let type_of_entry e =
match e with
- Ast _ -> ETast
- | ListAst _ -> ETastl
-
+ | Ast _ -> ETast
+ | ListAst _ -> ETastl
type gram_universe = (string, typed_entry) Hashtbl.t
-
let trace = ref false
-(*
-trace.val := True;
-*)
-
(* The univ_tab is not part of the state. It contains all the grammar that
exist or have existed before in the session. *)
-let univ_tab = Hashtbl.create 7
-let get_univ s =
- try Hashtbl.find univ_tab s with
- Not_found ->
- if !trace then
- begin Printf.eprintf "[Creating univ %s]\n" s; flush stderr; () end;
- let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u
+let univ_tab = Hashtbl.create 7
+let get_univ s =
+ try
+ Hashtbl.find univ_tab s
+ with Not_found ->
+ if !trace then begin
+ Printf.eprintf "[Creating univ %s]\n" s; flush stderr; ()
+ end;
+ let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u
+
let get_entry (u, utab) s =
- try Hashtbl.find utab s with
- Not_found -> errorlabstrm "Pcoq.get_entry"
- [< 'sTR"unknown grammar entry "; 'sTR u; 'sTR":"; 'sTR s >]
-
-
+ try
+ Hashtbl.find utab s
+ with Not_found ->
+ errorlabstrm "Pcoq.get_entry"
+ [< 'sTR"unknown grammar entry "; 'sTR u; 'sTR":"; 'sTR s >]
+
let new_entry etyp (u, utab) s =
let ename = u ^ ":" ^ s in
let e =
match etyp with
- ETast -> Ast (Gram.Entry.create ename)
- | ETastl -> ListAst (Gram.Entry.create ename)
+ | ETast -> Ast (Gram.Entry.create ename)
+ | ETastl -> ListAst (Gram.Entry.create ename)
in
Hashtbl.add utab s e; e
-
-
+
let create_entry (u, utab) s etyp =
try
let e = Hashtbl.find utab s in
if type_of_entry e <> etyp then
- failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type")
- else e
- with
- Not_found ->
- if !trace then
- begin
- Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; ()
- end;
- new_entry etyp (u, utab) s
-
-
+ failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type");
+ e
+ with Not_found ->
+ if !trace then begin
+ Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr; ()
+ end;
+ new_entry etyp (u, utab) s
+
let force_entry_type (u, utab) s etyp =
try
let entry = Hashtbl.find utab s in
let extyp = type_of_entry entry in
- if etyp = extyp then entry
- else
- begin
- prerr_endline
- ("Grammar entry " ^ u ^ ":" ^ s ^
- " redefined with another type;\n older entry hidden.");
- Hashtbl.remove utab s;
- new_entry etyp (u, utab) s
- end
- with
- Not_found -> new_entry etyp (u, utab) s
-
-
-
-
+ if etyp = extyp then
+ entry
+ else begin
+ prerr_endline
+ ("Grammar entry " ^ u ^ ":" ^ s ^
+ " redefined with another type;\n older entry hidden.");
+ Hashtbl.remove utab s;
+ new_entry etyp (u, utab) s
+ end
+ with Not_found ->
+ new_entry etyp (u, utab) s
(* Grammar entries *)
@@ -228,7 +211,7 @@ module Command =
let gec s =
let e = Gram.Entry.create ("Command." ^ s) in
Hashtbl.add ucommand s (Ast e); e
-
+
let gec_list s =
let e = Gram.Entry.create ("Command." ^ s) in
Hashtbl.add ucommand s (ListAst e); e
@@ -445,6 +428,7 @@ END
(* Quotations *)
open Prim
+
let define_quotation default s e =
(if default then
GEXTEND Gram
@@ -452,5 +436,5 @@ let define_quotation default s e =
END);
(GEXTEND Gram
ast:
- [ [ "<"; ":"; LIDENT $s$; ":"; "<"; c = e; ">>" -> c ] ];
+ [ [ "<"; ":"; IDENT $s$; ":"; "<"; c = e; ">>" -> c ] ];
END)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a33288189c..5a13274301 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -1,4 +1,6 @@
+(* $Id$ *)
+
let dummy_loc = (0,0)
let is_meta s = String.length s > 0 && s.[0] == '$'
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:27:06 +0000