diff options
| author | aspiwack | 2009-08-14 16:17:56 +0000 |
|---|---|---|
| committer | aspiwack | 2009-08-14 16:17:56 +0000 |
| commit | e3839529209cbd6955811be79cab57ed449edd6b (patch) | |
| tree | 19083521e83e9d4bc385b3cd163042e697d157d6 /plugins/interface | |
| parent | d1593f3524cfc1d0fdbd0194e05703d15dc9ba00 (diff) | |
+Fix interface.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12281 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface')
| -rw-r--r-- | plugins/interface/xlate.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index f60a9ee0bd..c27b10c63e 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -2182,16 +2182,16 @@ let rec xlate_vernac = | VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s) | VernacTime(v) -> CT_time(xlate_vernac v) | VernacTimeout(n,v) -> CT_timeout(CT_int n,xlate_vernac v) - | VernacSetOption (["Implicit"; "Arguments"], BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[]) + | VernacSetOption (_,["Implicit"; "Arguments"], BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[]) |VernacExactProof f -> CT_proof(xlate_formula f) - | VernacSetOption (table, BoolValue true) -> + | VernacSetOption (_,table, BoolValue true) -> let table1 = match table with [s] -> CT_coerce_ID_to_TABLE(CT_ident s) | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2) | _ -> xlate_error "TODO: arbitrary-length Table names" in CT_set_option(table1) - | VernacSetOption (table, v) -> + | VernacSetOption (_,table, v) -> let table1 = match table with [s] -> CT_coerce_ID_to_TABLE(CT_ident s) @@ -2205,7 +2205,7 @@ let rec xlate_vernac = | IntValue n -> CT_coerce_INT_to_SINGLE_OPTION_VALUE(CT_int n) in CT_set_option_value(table1, value) - | VernacUnsetOption(table) -> + | VernacUnsetOption(_,table) -> let table1 = match table with [s] -> CT_coerce_ID_to_TABLE(CT_ident s) |