diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ea686e5a3..d10a2950c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -637,11 +637,11 @@ GEXTEND Gram (* Pour intervenir sur les tables de paramčtres *) | "Set"; table = option_table; v = option_value -> - VernacSetOption (table,v) + VernacSetOption (use_locality_full(),table,v) | "Set"; table = option_table -> - VernacSetOption (table,BoolValue true) + VernacSetOption (use_locality_full(),table,BoolValue true) | IDENT "Unset"; table = option_table -> - VernacUnsetOption table + VernacUnsetOption (use_locality_full(),table) | IDENT "Print"; IDENT "Table"; table = option_table -> VernacPrintOption table @@ -779,10 +779,10 @@ GEXTEND Gram (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> - VernacSetOption (["Ltac";"Debug"], BoolValue true) + VernacSetOption (None,["Ltac";"Debug"], BoolValue true) | IDENT "Debug"; IDENT "Off" -> - VernacSetOption (["Ltac";"Debug"], BoolValue false) + VernacSetOption (None,["Ltac";"Debug"], BoolValue false) ] ]; END |