aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_basevernac.ml4162
-rw-r--r--parsing/g_proofs.ml4120
-rw-r--r--parsing/g_vernac.ml4149
3 files changed, 213 insertions, 218 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 031ec2831..4e4be99d5 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -63,159 +63,159 @@ GEXTEND Gram
GLOBAL: command;
command:
- [ [ IDENT "Pwd"; "." -> <:ast< (PWD) >>
- | IDENT "Cd"; "." -> <:ast< (CD) >>
- | IDENT "Cd"; dir = stringarg; "." -> <:ast< (CD $dir) >>
+ [ [ IDENT "Pwd" -> <:ast< (PWD) >>
+ | IDENT "Cd" -> <:ast< (CD) >>
+ | IDENT "Cd"; dir = stringarg -> <:ast< (CD $dir) >>
- | IDENT "Drop"; "." -> <:ast< (DROP) >>
- | IDENT "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP)>>
- | "Quit"; "." -> <:ast< (QUIT) >>
+ | IDENT "Drop" -> <:ast< (DROP) >>
+ | IDENT "ProtectedLoop" -> <:ast< (PROTECTEDLOOP)>>
+ | "Quit" -> <:ast< (QUIT) >>
- | IDENT "Print"; IDENT "All"; "." -> <:ast< (PrintAll) >>
- | IDENT "Print"; "." -> <:ast< (PRINT) >>
- | IDENT "Print"; IDENT "Hint"; "*"; "."
+ | IDENT "Print"; IDENT "All" -> <:ast< (PrintAll) >>
+ | IDENT "Print" -> <:ast< (PRINT) >>
+ | IDENT "Print"; IDENT "Hint"; "*"
-> <:ast< (PrintHint) >>
- | IDENT "Print"; IDENT "Hint"; s = identarg; "." ->
+ | IDENT "Print"; IDENT "Hint"; s = identarg ->
<:ast< (PrintHintId $s) >>
- | IDENT "Print"; IDENT "Hint"; "." ->
+ | IDENT "Print"; IDENT "Hint" ->
<:ast< (PrintHintGoal) >>
- | IDENT "Print"; IDENT "HintDb"; s = identarg ; "." ->
+ | IDENT "Print"; IDENT "HintDb"; s = identarg ->
<:ast< (PrintHintDb $s) >>
- | IDENT "Print"; IDENT "Section"; s = identarg; "." ->
+ | IDENT "Print"; IDENT "Section"; s = identarg ->
<:ast< (PrintSec $s) >>
- | IDENT "Print"; IDENT "States"; "." -> <:ast< (PrintStates) >>
+ | IDENT "Print"; IDENT "States" -> <:ast< (PrintStates) >>
(* This should be in "syntax" section but is here for factorization *)
- | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg; "." ->
+ | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg ->
<:ast< (PrintGrammar $uni $ent) >>
- | IDENT "Locate"; IDENT "File"; f = stringarg; "." ->
+ | IDENT "Locate"; IDENT "File"; f = stringarg ->
<:ast< (LocateFile $f) >>
- | IDENT "Locate"; IDENT "Library"; id = identarg; "." ->
+ | IDENT "Locate"; IDENT "Library"; id = identarg ->
<:ast< (LocateLibrary $id) >>
- | IDENT "Locate"; id = qualidarg; "." ->
+ | IDENT "Locate"; id = qualidarg ->
<:ast< (Locate $id) >>
(* Managing load paths *)
| IDENT "Add"; IDENT "LoadPath"; dir = stringarg;
- "as"; alias = qualidarg; "." -> <:ast< (ADDPATH $dir $alias) >>
- | IDENT "Add"; IDENT "LoadPath"; dir = stringarg; "." ->
+ "as"; alias = qualidarg -> <:ast< (ADDPATH $dir $alias) >>
+ | IDENT "Add"; IDENT "LoadPath"; dir = stringarg ->
<:ast< (ADDPATH $dir) >>
| IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = stringarg;
- "as"; alias=qualidarg; "." -> <:ast< (RECADDPATH $dir $alias) >>
- | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = stringarg; "." ->
+ "as"; alias=qualidarg -> <:ast< (RECADDPATH $dir $alias) >>
+ | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = stringarg ->
<:ast< (RECADDPATH $dir) >>
- | IDENT "Remove"; IDENT "LoadPath"; dir = stringarg; "." ->
+ | IDENT "Remove"; IDENT "LoadPath"; dir = stringarg ->
<:ast< (DELPATH $dir) >>
- | IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >>
+ | IDENT "Print"; IDENT "LoadPath" -> <:ast< (PrintPath) >>
(* For compatibility *)
- | IDENT "AddPath"; dir = stringarg; "as"; alias = qualidarg; "." ->
+ | IDENT "AddPath"; dir = stringarg; "as"; alias = qualidarg ->
<:ast< (ADDPATH $dir $alias) >>
- | IDENT "AddPath"; dir = stringarg; "." -> <:ast< (ADDPATH $dir) >>
- | IDENT "AddRecPath"; dir = stringarg; "as"; alias=qualidarg; "." ->
+ | IDENT "AddPath"; dir = stringarg -> <:ast< (ADDPATH $dir) >>
+ | IDENT "AddRecPath"; dir = stringarg; "as"; alias=qualidarg ->
<:ast< (RECADDPATH $dir $alias) >>
- | IDENT "AddRecPath"; dir = stringarg; "." ->
+ | IDENT "AddRecPath"; dir = stringarg ->
<:ast< (RECADDPATH $dir) >>
- | IDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >>
+ | IDENT "DelPath"; dir = stringarg -> <:ast< (DELPATH $dir) >>
- | IDENT "Print"; IDENT "Modules"; "." -> <:ast< (PrintModules) >>
- | IDENT "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 (CADUC) *)
- | IDENT "Print"; id = qualidarg; "." -> <:ast< (PrintId $id) >>
- | IDENT "Search"; id = qualidarg; l = in_or_out_modules; "." ->
+ | IDENT "Print"; id = qualidarg -> <:ast< (PrintId $id) >>
+ | IDENT "Search"; id = qualidarg; l = in_or_out_modules ->
<:ast< (SEARCH $id ($LIST $l)) >>
- | IDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >>
- | IDENT "SearchPattern"; c = constrarg; l = in_or_out_modules; "." ->
+ | IDENT "Inspect"; n = numarg -> <:ast< (INSPECT $n) >>
+ | IDENT "SearchPattern"; c = constrarg; l = in_or_out_modules ->
<:ast< (SearchPattern $c ($LIST $l)) >>
- | IDENT "SearchRewrite"; c = constrarg; l = in_or_out_modules; "." ->
+ | IDENT "SearchRewrite"; c = constrarg; l = in_or_out_modules ->
<:ast< (SearchRewrite $c ($LIST $l)) >>
(* TODO: rapprocher Eval et Check *)
- | IDENT "Eval"; r = Tactic.red_tactic; "in"; c = constrarg; "." ->
+ | IDENT "Eval"; r = Tactic.red_tactic; "in"; c = constrarg ->
<:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c) >>
| IDENT "Eval"; g = numarg; r = Tactic.red_tactic;
- "in"; c = constrarg; "." ->
+ "in"; c = constrarg ->
<:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c $g) >>
- | check = check_tok; c = constrarg; "." -> <:ast< (Check $check $c) >>
- | check = check_tok; g = numarg; c = constrarg; "." ->
+ | check = check_tok; c = constrarg -> <:ast< (Check $check $c) >>
+ | check = check_tok; g = numarg; c = constrarg ->
<:ast< (Check $check $c $g) >>
- | IDENT "Print"; IDENT "ML"; IDENT "Path"; "." ->
+ | IDENT "Print"; IDENT "ML"; IDENT "Path" ->
<:ast< (PrintMLPath) >>
- | IDENT "Print"; IDENT "ML"; IDENT "Modules"; "." ->
+ | IDENT "Print"; IDENT "ML"; IDENT "Modules" ->
<:ast< (PrintMLModules) >>
- | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = stringarg; "." ->
+ | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = stringarg ->
<:ast< (AddMLPath $dir) >>
| IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path";
- dir = stringarg; "." ->
+ dir = stringarg ->
<:ast< (RecAddMLPath $dir) >>
- | IDENT "Print"; IDENT "Graph"; "." -> <:ast< (PrintGRAPH) >>
- | IDENT "Print"; IDENT "Classes"; "." -> <:ast< (PrintCLASSES) >>
- | IDENT "Print"; IDENT "Coercions"; "." -> <:ast< (PrintCOERCIONS) >>
- | IDENT "Print"; IDENT "Coercion"; IDENT "Paths"; 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 "Coercion"; IDENT "Paths"; c = identarg; d = identarg ->
<:ast< (PrintPATH $c $d) >>
| IDENT "Time"; v = vernac -> <:ast< (Time $v)>>
- | IDENT "SearchIsos"; com = constrarg; "." ->
+ | IDENT "SearchIsos"; com = constrarg ->
<:ast< (Searchisos $com) >>
- | "Set"; IDENT "Undo"; n = numarg; "." ->
+ | "Set"; IDENT "Undo"; n = numarg ->
<:ast< (SETUNDO $n) >>
- | IDENT "Unset"; IDENT "Undo"; "." -> <:ast< (UNSETUNDO) >>
- | "Set"; IDENT "Hyps_limit"; n = numarg; "." ->
+ | IDENT "Unset"; IDENT "Undo" -> <:ast< (UNSETUNDO) >>
+ | "Set"; IDENT "Hyps_limit"; n = numarg ->
<:ast< (SETHYPSLIMIT $n) >>
- | IDENT "Unset"; IDENT "Hyps_limit"; "." ->
+ | IDENT "Unset"; IDENT "Hyps_limit" ->
<:ast< (UNSETHYPSLIMIT) >>
(* Standardized syntax for Implicit Arguments *)
- | "Set"; IDENT "Implicit"; IDENT "Arguments"; "." ->
+ | "Set"; IDENT "Implicit"; IDENT "Arguments" ->
<:ast< (IMPLICIT_ARGS_ON) >>
- | IDENT "Unset"; IDENT "Implicit"; IDENT "Arguments"; "." ->
+ | IDENT "Unset"; IDENT "Implicit"; IDENT "Arguments" ->
<:ast< (IMPLICIT_ARGS_OFF) >>
- | IDENT "Test"; IDENT "Implicit"; IDENT "Arguments"; "." ->
+ | IDENT "Test"; IDENT "Implicit"; IDENT "Arguments" ->
<:ast< (TEST_IMPLICIT_ARGS) >>
(* Pour intervenir sur les tables de paramètres *)
| "Set"; table = identarg; field = identarg;
- value = option_value; "." ->
+ value = option_value ->
<:ast< (SetTableField $table $field $value) >>
- | "Set"; table = identarg; field = identarg; "." ->
+ | "Set"; table = identarg; field = identarg ->
<:ast< (SetTableField $table $field) >>
- | IDENT "Unset"; table = identarg; field = identarg; "." ->
+ | IDENT "Unset"; table = identarg; field = identarg ->
<:ast< (UnsetTableField $table $field) >>
- | "Set"; table = identarg; value = option_value; "." ->
+ | "Set"; table = identarg; value = option_value ->
<:ast< (SetTableField $table $value) >>
- | "Set"; table = identarg; "." ->
+ | "Set"; table = identarg ->
<:ast< (SetTableField $table) >>
- | IDENT "Unset"; table = identarg; "." ->
+ | IDENT "Unset"; table = identarg ->
<:ast< (UnsetTableField $table) >>
| IDENT "Print"; IDENT "Table";
- table = identarg; field = identarg; "." ->
+ table = identarg; field = identarg ->
<:ast< (PrintOption $table $field) >>
(* Le cas suivant inclut aussi le "Print id" standard *)
- | IDENT "Print"; IDENT "Table"; table = identarg; "." ->
+ | IDENT "Print"; IDENT "Table"; table = identarg ->
<:ast< (PrintOption $table) >>
- | IDENT "Add"; table = identarg; field = identarg; id = identarg; "."
+ | IDENT "Add"; table = identarg; field = identarg; id = identarg
-> <:ast< (AddTableField $table $field $id) >>
- | IDENT "Add"; table = identarg; field = identarg; id = stringarg; "."
+ | IDENT "Add"; table = identarg; field = identarg; id = stringarg
-> <:ast< (AddTableField $table $field $id) >>
- | IDENT "Add"; table = identarg; id = identarg; "."
+ | IDENT "Add"; table = identarg; id = identarg
-> <:ast< (AddTableField $table $id) >>
- | IDENT "Add"; table = identarg; id = stringarg; "."
+ | IDENT "Add"; table = identarg; id = stringarg
-> <:ast< (AddTableField $table $id) >>
- | IDENT "Test"; table = identarg; field = identarg; id = identarg; "."
+ | IDENT "Test"; table = identarg; field = identarg; id = identarg
-> <:ast< (MemTableField $table $field $id) >>
- | IDENT "Test"; table = identarg; field = identarg; id = stringarg; "."
+ | IDENT "Test"; table = identarg; field = identarg; id = stringarg
-> <:ast< (MemTableField $table $field $id) >>
- | IDENT "Test"; table = identarg; id = identarg; "."
+ | IDENT "Test"; table = identarg; id = identarg
-> <:ast< (MemTableField $table $id) >>
- | IDENT "Test"; table = identarg; id = stringarg; "."
+ | IDENT "Test"; table = identarg; id = stringarg
-> <:ast< (MemTableField $table $id) >>
- | IDENT "Remove"; table = identarg; field = identarg; id = identarg; "." ->
+ | IDENT "Remove"; table = identarg; field = identarg; id = identarg ->
<:ast< (RemoveTableField $table $field $id) >>
- | IDENT "Remove"; table = identarg; field = identarg; id = stringarg; "." ->
+ | IDENT "Remove"; table = identarg; field = identarg; id = stringarg ->
<:ast< (RemoveTableField $table $field $id) >>
- | IDENT "Remove"; table = identarg; id = identarg; "." ->
+ | IDENT "Remove"; table = identarg; id = identarg ->
<:ast< (RemoveTableField $table $id) >>
- | IDENT "Remove"; table = identarg; id = stringarg; "." ->
+ | IDENT "Remove"; table = identarg; id = stringarg ->
<:ast< (RemoveTableField $table $id) >> ] ]
;
option_value:
@@ -244,20 +244,20 @@ GEXTEND Gram
let _ = set_default_action_parser_by_name univ in univ ] ]
;
syntax:
- [ [ IDENT "Token"; s = STRING; "." -> <:ast< (TOKEN ($STR $s)) >>
+ [ [ IDENT "Token"; s = STRING -> <:ast< (TOKEN ($STR $s)) >>
| "Grammar"; univ = univ;
- tl = LIST1 Prim.grammar_entry SEP "with"; "." ->
+ tl = LIST1 Prim.grammar_entry SEP "with" ->
<:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >>
- | "Syntax"; univ = univ; el=LIST1 Prim.syntax_entry SEP ";"; "." ->
+ | "Syntax"; univ = univ; el=LIST1 Prim.syntax_entry SEP ";" ->
<:ast< (SYNTAX ($VAR univ) (ASTLIST ($LIST el))) >>
(* Faudrait une version de qualidarg dans Prim pour respecter l'ordre *)
| IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string;
- p = qualidarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >>
+ p = qualidarg -> <:ast< (INFIX (AST $as_) $n $op $p) >>
| IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string;
- p = qualidarg; "." -> <:ast< (DISTFIX (AST $as_) $n $s $p) >>
+ p = qualidarg -> <:ast< (DISTFIX (AST $as_) $n $s $p) >>
(* "Print" "Grammar" should be here but is in "command" entry in order
to factorize with other "Print"-based vernac entries *)
] ]
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index c1b0c9660..d176a05aa 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -34,76 +34,76 @@ GEXTEND Gram
<:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ]
;
command:
- [ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >>
- | IDENT "Goal"; "." -> <:ast< (GOAL) >>
- | "Proof"; "." -> <:ast< (GOAL) >>
- | IDENT "Begin"; "." -> <:ast< (GOAL) >>
- | IDENT "Abort"; "." -> <:ast< (ABORT) >>
- | "Qed"; "." -> <:ast< (SaveNamed) >>
- | IDENT "Save"; "." -> <:ast< (SaveNamed) >>
- | IDENT "Defined"; "." -> <:ast< (DefinedNamed) >>
- | IDENT "Defined"; id = identarg; "." -> <:ast< (DefinedAnonymous $id) >>
- | IDENT "Save"; IDENT "Remark"; id = identarg; "." ->
+ [ [ IDENT "Goal"; c = constrarg -> <:ast< (GOAL $c) >>
+ | IDENT "Goal" -> <:ast< (GOAL) >>
+ | "Proof" -> <:ast< (GOAL) >>
+ | IDENT "Begin" -> <:ast< (GOAL) >>
+ | IDENT "Abort" -> <:ast< (ABORT) >>
+ | "Qed" -> <:ast< (SaveNamed) >>
+ | IDENT "Save" -> <:ast< (SaveNamed) >>
+ | IDENT "Defined" -> <:ast< (DefinedNamed) >>
+ | IDENT "Defined"; id = identarg -> <:ast< (DefinedAnonymous $id) >>
+ | IDENT "Save"; IDENT "Remark"; id = identarg ->
<:ast< (SaveAnonymousRmk $id) >>
- | IDENT "Save"; IDENT "Theorem"; id = identarg; "." ->
+ | IDENT "Save"; IDENT "Theorem"; id = identarg ->
<:ast< (SaveAnonymousThm $id) >>
- | IDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymous $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 = constrarg; "." -> <:ast< (PROOF $c) >>
- | 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; "." ->
+ | IDENT "Save"; id = identarg -> <:ast< (SaveAnonymous $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 = constrarg -> <:ast< (PROOF $c) >>
+ | 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) >>
- | 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 = constrarg; "." ->
+ | 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 = constrarg ->
<:ast< (EXISTENTIAL $n $c) >>
| IDENT "Existential"; n = numarg; ":="; c1 = Constr.constr; ":";
- c2 = Constr.constr; "." ->
+ c2 = Constr.constr ->
<:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
| IDENT "Existential"; n = numarg; ":"; c2 = Constr.constr; ":=";
- c1 = Constr.constr; "." ->
+ c1 = Constr.constr ->
<:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
- | IDENT "Explain"; "Proof"; l = numarg_list; "." ->
+ | IDENT "Explain"; "Proof"; l = numarg_list ->
<:ast< (ExplainProof ($LIST $l)) >>
- | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list; "." ->
+ | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list ->
<:ast< (ExplainProofTree ($LIST $l)) >>
- | 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) >>
+ | 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) >>
(* Definitions for tactics *)
- | deftok; "Definition"; name=identarg; ":="; body=Tactic.tactic;
- "." -> <:ast<(TACDEF $name (AST $body))>>
+ | deftok; "Definition"; name=identarg; ":="; body=Tactic.tactic
+ -> <:ast<(TACDEF $name (AST $body))>>
| deftok; "Definition"; name=identarg; largs=LIST1 input_fun;
- ":="; body=Tactic.tactic; "." ->
+ ":="; body=Tactic.tactic ->
<:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
- | IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause ; "." ->
+ | IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause ->
(match vc with
Coqast.Node(_,"RECCLAUSE",nme::tl) ->
<:ast<(TACDEF $nme (AST (REC $vc)))>>
|_ ->
anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">])
|IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause;
- IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." ->
+ IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And" ->
let nvcl=
List.fold_right
(fun e b -> match e with
@@ -118,36 +118,36 @@ GEXTEND Gram
(* Hints for Auto and EAuto *)
| IDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":=";
- IDENT "Resolve"; c = constrarg; "." ->
+ IDENT "Resolve"; c = constrarg ->
<:ast<(HintResolve $hintname (VERNACARGLIST ($LIST $dbname)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- IDENT "Immediate"; c = constrarg; "." ->
+ IDENT "Immediate"; c = constrarg ->
<:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- IDENT "Unfold"; c = identarg; "." ->
+ IDENT "Unfold"; c = identarg ->
<:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- IDENT "Constructors"; c = qualidarg; "." ->
+ IDENT "Constructors"; c = qualidarg ->
<:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- IDENT "Extern"; n = numarg; c = constrarg ; tac = tacarg; "." ->
+ IDENT "Extern"; n = numarg; c = constrarg ; tac = tacarg ->
<:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames))
$n $c (TACTIC $tac))>>
| IDENT "Hints"; IDENT "Resolve"; l = ne_qualidarg_list;
- dbnames = opt_identarg_list; "." ->
+ dbnames = opt_identarg_list ->
<:ast< (HintsResolve (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
| IDENT "Hints"; IDENT "Immediate"; l = ne_qualidarg_list;
- dbnames = opt_identarg_list; "." ->
+ dbnames = opt_identarg_list ->
<:ast< (HintsImmediate (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
| IDENT "Hints"; IDENT "Unfold"; l = ne_qualidarg_list;
- dbnames = opt_identarg_list; "." ->
+ dbnames = opt_identarg_list ->
<:ast< (HintsUnfold (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
| IDENT "HintDestruct";
@@ -155,14 +155,14 @@ GEXTEND Gram
na = identarg;
hyptyp = constrarg;
pri = numarg;
- tac = Prim.astact; "." ->
+ tac = Prim.astact ->
<:ast< (HintDestruct $na (AST $dloc) $hyptyp $pri (AST $tac))>>
- | n = numarg; ":"; tac = tacarg; "." ->
+ | n = numarg; ":"; tac = tacarg ->
<:ast< (SOLVE $n (TACTIC $tac)) >>
(*This entry is not commented, only for debug*)
- | IDENT "PrintConstr"; com = constrarg; "." ->
+ | IDENT "PrintConstr"; com = constrarg ->
<:ast< (PrintConstr $com)>>
] ];
END
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 60b0cb5c1..c0b8e45ab 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -15,10 +15,12 @@ open Vernac
GEXTEND Gram
GLOBAL: vernac;
vernac:
- [ [ g = gallina -> g
- | g = gallina_ext -> g
- | c = command -> c
- | c = syntax -> c
+ (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
+ (* "." is still in the stream and discard_to_dot works correctly *)
+ [ [ g = gallina; "." -> g
+ | g = gallina_ext; "." -> g
+ | c = command; "." -> c
+ | c = syntax; "." -> c
| "["; l = vernac_list_tail -> <:ast< (VernacList ($LIST $l)) >> ] ]
;
vernac: LAST
@@ -39,9 +41,9 @@ GEXTEND Gram
GLOBAL: gallina gallina_ext;
theorem_body_line:
- [ [ n = numarg; ":"; tac = tacarg; "." ->
+ [ [ n = numarg; ":"; tac = tacarg ->
<:ast< (VERNACCALL {SOLVE} $n (TACTIC $tac)) >>
- | tac = tacarg; "." -> <:ast< (VERNACCALL {SOLVE} 1 (TACTIC $tac)) >>
+ | tac = tacarg -> <:ast< (VERNACCALL {SOLVE} 1 (TACTIC $tac)) >>
] ]
;
theorem_body_line_list:
@@ -103,40 +105,40 @@ GEXTEND Gram
;
gallina:
(* Definition, Goal *)
- [ [ thm = thm_tok; id = identarg; ":"; c = constrarg; "." ->
+ [ [ thm = thm_tok; id = identarg; ":"; c = constrarg ->
<:ast< (StartProof $thm $id $c) >>
| thm = thm_tok; id = identarg; ":"; c = constrarg; ":="; "Proof";
- tb = theorem_body; "Qed"; "." ->
+ tb = theorem_body; "Qed" ->
<:ast< (TheoremProof $thm $id $c $tb) >>
| def = def_tok; s = identarg; bl = binders_list;
- ":"; t = Constr.constr; "." ->
+ ":"; t = Constr.constr ->
<:ast< (StartProof $def $s (CONSTR ($ABSTRACT "PRODLIST" $bl $t))) >>
| def = def_tok; s = identarg; bl = binders_list;
- ":="; red = reduce; c = Constr.constr; "." ->
+ ":="; red = reduce; c = Constr.constr ->
<:ast< (DEFINITION $def $s (CONSTR ($ABSTRACT "LAMBDALIST" $bl $c))
($LIST $red)) >>
| def = def_tok; s = identarg; bl = binders_list;
- ":="; red = reduce; c = Constr.constr; ":"; t = Constr.constr; "." ->
+ ":="; red = reduce; c = Constr.constr; ":"; t = Constr.constr ->
<:ast< (DEFINITION $def $s (CONSTR ($ABSTRACT "LAMBDALIST" $bl $c))
(CONSTR ($ABSTRACT "PRODLIST" $bl $t)) ($LIST $red)) >>
| def = def_tok; s = identarg; bl = binders_list;
- ":"; t = Constr.constr; ":="; red = reduce; c = Constr.constr; "." ->
+ ":"; t = Constr.constr; ":="; red = reduce; c = Constr.constr ->
<:ast< (DEFINITION $def $s (CONSTR ($ABSTRACT "LAMBDALIST" $bl $c))
(CONSTR ($ABSTRACT "PRODLIST" $bl $t)) ($LIST $red)) >>
- | hyp = hyp_tok; bl = ne_params_list; "." ->
+ | hyp = hyp_tok; bl = ne_params_list ->
<:ast< (VARIABLE $hyp (BINDERLIST ($LIST $bl))) >>
- | hyp = hyps_tok; bl = ne_params_list; "." ->
+ | hyp = hyps_tok; bl = ne_params_list ->
<:ast< (VARIABLE $hyp (BINDERLIST ($LIST $bl))) >>
- | hyp = param_tok; bl = ne_params_list; "." ->
+ | hyp = param_tok; bl = ne_params_list ->
<:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
- | hyp = params_tok; bl = ne_params_list; "." ->
+ | hyp = params_tok; bl = ne_params_list ->
<:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
] ]
;
gallina_ext:
[ [ IDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]";
- ":="; c = constrarg; "." ->
+ ":="; c = constrarg ->
<:ast< (ABSTRACTION $id $c ($LIST $l)) >>
] ]
;
@@ -270,37 +272,37 @@ GEXTEND Gram
;
gallina_ext:
[ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_tok;
- indl = block_old_style; "." ->
+ indl = block_old_style ->
<:ast< (OLDMUTUALINDUCTIVE (BINDERLIST ($LIST $bl)) $f
(VERNACARGLIST ($LIST $indl))) >>
| record_tok; oc = opt_coercion; name = identarg; ps = indpar; ":";
- s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}"; "." ->
+ s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}" ->
<:ast< (RECORD ($STR $oc) $name $ps $s $c $fs) >>
(* | record_tok; ">"; name = identarg; ps = indpar; ":";
- s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}"; "." ->
+ s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}" ->
<:ast< (RECORD "COERCION" $name $ps $s $c $fs) >>
*) ] ]
;
gallina:
- [ [ IDENT "Mutual"; f = finite_tok; indl = block; "." ->
+ [ [ IDENT "Mutual"; f = finite_tok; indl = block ->
<:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >>
- | "Fixpoint"; recs = specifrec; "." ->
+ | "Fixpoint"; recs = specifrec ->
<:ast< (MUTUALRECURSIVE (VERNACARGLIST ($LIST $recs))) >>
- | "CoFixpoint"; corecs = specifcorec; "." ->
+ | "CoFixpoint"; corecs = specifcorec ->
<:ast< (MUTUALCORECURSIVE (VERNACARGLIST ($LIST $corecs))) >>
- | IDENT "Scheme"; schemes = specifscheme; "." ->
+ | IDENT "Scheme"; schemes = specifscheme ->
<:ast< (INDUCTIONSCHEME (VERNACARGLIST ($LIST $schemes))) >>
| f = finite_tok; s = sortarg; id = identarg; indpar = indpar; ":=";
- lc = constructor_list; "." ->
+ lc = constructor_list ->
<:ast< (ONEINDUCTIVE $f $id $s $indpar $lc) >>
- | f = finite_tok; indl = block; "." ->
+ | f = finite_tok; indl = block ->
<:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >>
| record_tok; oc = opt_coercion; name = identarg; ps = indpar; ":";
- s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}"; "." ->
+ s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}" ->
<:ast< (RECORD ($STR $oc) $name $ps $s $c $fs) >>
(* | record_tok; ">"; name = identarg; ps = indpar; ":";
- s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}"; "." ->
+ s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}" ->
<:ast< (RECORD "COERCION" $name $ps $s $c $fs) >>
*) ] ];
@@ -318,61 +320,54 @@ GEXTEND Gram
gallina_ext:
[ [
(* Sections *)
- IDENT "Section"; id = identarg; "." -> <:ast< (BeginSection $id) >>
- | IDENT "Chapter"; id = identarg; "." -> <:ast< (BeginSection $id) >>
- | IDENT "Module"; id = identarg; "." -> <:ast< (BeginModule $id) >>
- | IDENT "End"; id = identarg; "." -> <:ast< (EndSection $id) >>
+ IDENT "Section"; id = identarg -> <:ast< (BeginSection $id) >>
+ | IDENT "Chapter"; id = identarg -> <:ast< (BeginSection $id) >>
+ | IDENT "Module"; id = identarg -> <:ast< (BeginModule $id) >>
+ | IDENT "End"; id = identarg -> <:ast< (EndSection $id) >>
(* Transparent and Opaque *)
- | IDENT "Transparent"; l = ne_qualidconstarg_list; "." ->
+ | IDENT "Transparent"; l = ne_qualidconstarg_list ->
<:ast< (TRANSPARENT ($LIST $l)) >>
- | IDENT "Opaque"; l = ne_qualidconstarg_list; "." ->
+ | IDENT "Opaque"; l = ne_qualidconstarg_list ->
<:ast< (OPAQUE ($LIST $l)) >>
(* Coercions *)
- (* BUG: "Coercion S.T := A." n'est pas reconnu comme une phrase, pq?? *)
- | IDENT "Coercion"; qid = qualidarg; ":="; c = def_body; "." ->
+ | IDENT "Coercion"; qid = qualidarg; ":="; c = def_body ->
let s = Ast.coerce_to_var "qid" qid in
<:ast< (DEFINITION "COERCION" ($VAR $s) $c) >>
-(*
- | IDENT "Coercion"; qid = qualidarg; ":="; c1 = Constr.constr; ":";
- c2 = Constr.constr; "." ->
- let s = Ast.coerce_to_var "qid" qid in
- <:ast< (DEFINITION "COERCION" ($VAR $s) (CONSTR (CAST $c1 $c2))) >>
-*)
| IDENT "Coercion"; IDENT "Local"; s = identarg; ":=";
- c = constrarg; "." ->
+ c = constrarg ->
<:ast< (DEFINITION "LCOERCION" $s $c) >>
| IDENT "Coercion"; IDENT "Local"; s = identarg; ":=";
- c1 = Constr.constr; ":"; c2 = Constr.constr; "." ->
+ c1 = Constr.constr; ":"; c2 = Constr.constr ->
<:ast< (DEFINITION "LCOERCION" $s (CONSTR (CAST $c1 $c2))) >>
| IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = qualidarg;
- ":"; c = qualidarg; ">->"; d = qualidarg; "." ->
+ ":"; c = qualidarg; ">->"; d = qualidarg ->
<:ast< (COERCION "LOCAL" "IDENTITY" $f $c $d) >>
| IDENT "Identity"; IDENT "Coercion"; f = qualidarg; ":";
- c = qualidarg; ">->"; d = qualidarg; "." ->
+ c = qualidarg; ">->"; d = qualidarg ->
<:ast< (COERCION "" "IDENTITY" $f $c $d) >>
| IDENT "Coercion"; IDENT "Local"; f = qualidarg; ":"; c = qualidarg;
- ">->"; d = qualidarg; "." ->
+ ">->"; d = qualidarg ->
<:ast< (COERCION "LOCAL" "" $f $c $d) >>
| IDENT "Coercion"; f = qualidarg; ":"; c = qualidarg; ">->";
- d = qualidarg; "." -> <:ast< (COERCION "" "" $f $c $d) >>
- | IDENT "Class"; IDENT "Local"; c = qualidarg; "." ->
+ d = qualidarg -> <:ast< (COERCION "" "" $f $c $d) >>
+ | IDENT "Class"; IDENT "Local"; c = qualidarg ->
<:ast< (CLASS "LOCAL" $c) >>
- | IDENT "Class"; c = qualidarg; "." -> <:ast< (CLASS "" $c) >>
+ | IDENT "Class"; c = qualidarg -> <:ast< (CLASS "" $c) >>
(* Implicit *)
+ | IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = constrarg
+ -> <:ast< (SyntaxMacro $id $com) >>
| IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = constrarg;
- "." -> <:ast< (SyntaxMacro $id $com) >>
- | IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = constrarg;
- "|"; n = numarg; "." -> <:ast< (SyntaxMacro $id $com $n) >>
- | IDENT "Implicit"; IDENT "Arguments"; IDENT "On"; "." ->
+ "|"; n = numarg -> <:ast< (SyntaxMacro $id $com $n) >>
+ | IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
<:ast< (IMPLICIT_ARGS_ON) >>
- | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off"; "." ->
+ | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off" ->
<:ast< (IMPLICIT_ARGS_OFF) >>
- | IDENT "Implicits"; id = identarg; "["; l = numarg_list; "]"; "." ->
+ | IDENT "Implicits"; id = identarg; "["; l = numarg_list; "]" ->
<:ast< (IMPLICITS "" $id ($LIST $l)) >>
- | IDENT "Implicits"; id = identarg; "." ->
+ | IDENT "Implicits"; id = identarg ->
<:ast< (IMPLICITS "Auto" $id) >>
] ]
;
@@ -394,7 +389,7 @@ GEXTEND Gram
;
command:
[ [ "Load"; verbosely = [ IDENT "Verbose" -> "Verbose" | -> "" ];
- s = [ s = STRING -> s | s = IDENT -> s ]; "." ->
+ s = [ s = STRING -> s | s = IDENT -> s ] ->
<:ast< (LoadFile ($STR $verbosely) ($STR $s)) >>
| "Compile";
verbosely =
@@ -405,24 +400,24 @@ GEXTEND Gram
[ IDENT "Specification" -> "Specification"
| -> "" ];
mname = [ s = STRING -> s | s = IDENT -> s ];
- fname = OPT [ s = STRING -> s | s = IDENT -> s ]; "." ->
+ fname = OPT [ s = STRING -> s | s = IDENT -> s ] ->
let fname = match fname with Some s -> s | None -> mname in
<:ast< (CompileFile ($STR $verbosely) ($STR $only_spec)
($STR $mname) ($STR $fname))>>
- | IDENT "Read"; IDENT "Module"; id = identarg; "." ->
+ | IDENT "Read"; IDENT "Module"; id = identarg ->
<:ast< (ReadModule $id) >>
| IDENT "Require"; import = import_tok; specif = specif_tok;
- id = identarg; "." -> <:ast< (Require $import $specif $id) >>
+ id = identarg -> <:ast< (Require $import $specif $id) >>
| IDENT "Require"; import = import_tok; specif = specif_tok;
- id = identarg; filename = stringarg; "." ->
+ id = identarg; filename = stringarg ->
<:ast< (RequireFrom $import $specif $id $filename) >>
- | IDENT "Write"; IDENT "Module"; id = identarg; "." ->
+ | IDENT "Write"; IDENT "Module"; id = identarg ->
<:ast< (WriteModule $id) >>
- | IDENT "Write"; IDENT "Module"; id = identarg; s = stringarg; "." ->
+ | IDENT "Write"; IDENT "Module"; id = identarg; s = stringarg ->
<:ast< (WriteModule $id $s) >>
| IDENT "Declare"; IDENT "ML"; IDENT "Module";
- l = ne_stringarg_list; "." -> <:ast< (DeclareMLModule ($LIST $l)) >>
- | IDENT "Import"; id = identarg; "." -> <:ast< (ImportModule $id) >>
+ l = ne_stringarg_list -> <:ast< (DeclareMLModule ($LIST $l)) >>
+ | IDENT "Import"; id = identarg -> <:ast< (ImportModule $id) >>
]
]
@@ -436,27 +431,27 @@ GEXTEND Gram
[ [
(* State management *)
- IDENT "Write"; IDENT "State"; id = identarg; "." ->
+ IDENT "Write"; IDENT "State"; id = identarg ->
<:ast< (WriteState $id) >>
- | IDENT "Write"; IDENT "State"; s = stringarg; "." ->
+ | IDENT "Write"; IDENT "State"; s = stringarg ->
<:ast< (WriteState $s) >>
- | IDENT "Restore"; IDENT "State"; id = identarg; "." ->
+ | IDENT "Restore"; IDENT "State"; id = identarg ->
<:ast< (RestoreState $id) >>
- | IDENT "Restore"; IDENT "State"; s = stringarg; "." ->
+ | IDENT "Restore"; IDENT "State"; s = stringarg ->
<:ast< (RestoreState $s) >>
- | IDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >>
- | IDENT "Reset"; IDENT "Initial"; "." -> <:ast< (ResetInitial) >>
- | IDENT "Reset"; IDENT "Section"; id = identarg; "." ->
+ | IDENT "Reset"; id = identarg -> <:ast< (ResetName $id) >>
+ | IDENT "Reset"; IDENT "Initial" -> <:ast< (ResetInitial) >>
+ | IDENT "Reset"; IDENT "Section"; id = identarg ->
<:ast< (ResetSection $id) >>
(* Extraction *)
- | IDENT "Extraction"; id = identarg; "." ->
+ | IDENT "Extraction"; id = identarg ->
<:ast< (PrintExtractId $id) >>
- | IDENT "Extraction"; "." -> <:ast< (PrintExtract) >>
+ | IDENT "Extraction" -> <:ast< (PrintExtract) >>
(* Tactic Debugger *)
- | IDENT "Debug"; IDENT "On"; "." -> <:ast< (DebugOn) >>
- | IDENT "Debug"; IDENT "Off"; "." -> <:ast< (DebugOff) >>
+ | IDENT "Debug"; IDENT "On" -> <:ast< (DebugOn) >>
+ | IDENT "Debug"; IDENT "Off" -> <:ast< (DebugOff) >>
] ];
END
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 21:09:47 +0000