diff options
| author | Pierre-Marie Pédrot | 2016-03-17 15:10:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-17 15:10:57 +0100 |
| commit | e3e8a4065047e254f5f5c2747227db75f01b7bed (patch) | |
| tree | c7505db28eee92bc1855b6ee0cf275381b4aa106 /tactics | |
| parent | 22c1e7c3f1d86902b1abf2d887e0e9bf93ddb60d (diff) | |
| parent | 2537e84ba9fa92db6cfd3d7f5e400b1716c31246 (diff) | |
Removing the default value mechanism for generic arguments.
There was a complicated dedicated code in grammar/ to decide whether a generic argument
parsed the empty string. We now only rely on a dynamic decision. This should not affect
efficiency, as it is only made once by declaration of ML tactics.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 4 | ||||
| -rw-r--r-- | tactics/g_rewrite.ml4 | 2 | ||||
| -rw-r--r-- | tactics/taccoerce.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tauto.ml | 2 |
5 files changed, 7 insertions, 7 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 85b9d6a08f..ae8b83b95e 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -931,9 +931,9 @@ type cmp = type 'i test = | Test of cmp * 'i * 'i -let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 None "cmp" +let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp" let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type = - Genarg.make0 None "tactest" + Genarg.make0 "tactest" let pr_cmp = function | Eq -> Pp.str"=" diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 6b6dc7b21a..8b012aa88e 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -184,7 +184,7 @@ END type binders_argtype = local_binder list let wit_binders = - (Genarg.create_arg None "binders" : binders_argtype Genarg.uniform_genarg_type) + (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) let binders = Pcoq.create_generic_entry "binders" (Genarg.rawwit wit_binders) diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 0cd3e09446..358f6d6468 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -18,11 +18,11 @@ open Constrarg exception CannotCoerceTo of string let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) = - Genarg.create_arg None "constr_context" + Genarg.create_arg "constr_context" (* includes idents known to be bound and references *) let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) = - Genarg.create_arg None "constr_under_binders" + Genarg.create_arg "constr_under_binders" let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit -> let Val.Dyn (t, _) = v in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 32f7c3c61c..36faba1137 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -109,7 +109,7 @@ type tacvalue = | VRec of value Id.Map.t ref * glob_tactic_expr let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = - Genarg.create_arg None "tacvalue" + Genarg.create_arg "tacvalue" let of_tacvalue v = in_gen (topwit wit_tacvalue) v let to_tacvalue v = out_gen (topwit wit_tacvalue) v diff --git a/tactics/tauto.ml b/tactics/tauto.ml index d3e0b1f449..a86fdb98a9 100644 --- a/tactics/tauto.ml +++ b/tactics/tauto.ml @@ -55,7 +55,7 @@ type tauto_flags = { } let wit_tauto_flags : tauto_flags uniform_genarg_type = - Genarg.create_arg None "tauto_flags" + Genarg.create_arg "tauto_flags" let assoc_flags ist = let v = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in |