diff options
Diffstat (limited to 'parsing/g_basevernac.ml4')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 31 |
1 files changed, 26 insertions, 5 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index e1c2191057..ec7c84b47b 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -91,16 +91,29 @@ GEXTEND Gram | IDENT "Locate"; id = qualidarg; "." -> <:ast< (Locate $id) >> - (* For compatibility (now turned into a table) *) - | IDENT "AddPath"; dir = stringarg; IDENT "As"; alias = qualidarg; "." -> + (* Managing load paths *) + | 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; "." -> + <:ast< (RECADDPATH $dir) >> + | IDENT "Remove"; IDENT "LoadPath"; dir = stringarg; "." -> + <:ast< (DELPATH $dir) >> + | IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >> + + (* For compatibility *) + | IDENT "AddPath"; dir = stringarg; "as"; alias = qualidarg; "." -> <:ast< (ADDPATH $dir $alias) >> | IDENT "AddPath"; dir = stringarg; "." -> <:ast< (ADDPATH $dir) >> - | IDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >> - | IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >> - | IDENT "AddRecPath"; dir = stringarg;IDENT "As"; alias=qualidarg; "." -> + | IDENT "AddRecPath"; dir = stringarg; "as"; alias=qualidarg; "." -> <:ast< (RECADDPATH $dir $alias) >> | IDENT "AddRecPath"; dir = stringarg; "." -> <:ast< (RECADDPATH $dir) >> + | IDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >> + | IDENT "Print"; IDENT "Modules"; "." -> <:ast< (PrintModules) >> | IDENT "Print"; "Proof"; id = identarg; "." -> <:ast< (PrintOpaqueId $id) >> @@ -147,6 +160,14 @@ GEXTEND Gram | IDENT "Unset"; IDENT "Hyps_limit"; "." -> <:ast< (UNSETHYPSLIMIT) >> + (* Standardized syntax for Implicit Arguments *) + | "Set"; IDENT "Implicit"; IDENT "Arguments"; "." -> + <:ast< (IMPLICIT_ARGS_ON) >> + | IDENT "Unset"; IDENT "Implicit"; IDENT "Arguments"; "." -> + <:ast< (IMPLICIT_ARGS_OFF) >> + | 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; "." -> |