From 25dde2366a4db47e5da13b2bbe4d03a31235706f Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 2 Aug 2009 19:51:48 +0000 Subject: Improved parameterization of Coq: - add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/interface/xlate.ml | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'plugins/interface') diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 6f9e673a92..bff8cae260 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -404,7 +404,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function | CPrim (_, String _) -> xlate_error "CPrim (String): TODO" | CHole _ -> CT_existvarc (* I assume CDynamic has been inserted to make free form extension of - the language possible, but this would go agains the logic of pcoq anyway. *) + the language possible, but this would go against the logic of pcoq anyway. *) | CDynamic (_, _) -> assert false | CDelimiters (_, key, num) -> CT_num_encapsulator(CT_num_type key , xlate_formula num) @@ -2179,21 +2179,21 @@ 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 (Goptions.SecondaryTable ("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) -> let table1 = match table with - PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) - | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in + [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) -> let table1 = match table with - PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) - | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in + [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 let value = match v with | BoolValue _ -> assert false @@ -2205,9 +2205,9 @@ let rec xlate_vernac = | VernacUnsetOption(table) -> let table1 = match table with - PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) - | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in + [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_unset_option(table1) | VernacAddOption (table, l) -> let values = @@ -2221,9 +2221,9 @@ let rec xlate_vernac = match values with [] -> assert false | a::b -> (a,b) in let table1 = match table with - PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) - | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in + [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_value2(table1, CT_id_or_string_ne_list(fst, values1)) | VernacImport(true, a::l) -> CT_export_id(CT_id_ne_list(reference_to_ct_ID a, -- cgit v1.2.3