diff options
| author | Pierre-Marie Pédrot | 2015-12-18 18:04:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-21 19:36:38 +0100 |
| commit | 5835804bd69a193b9ea29b6d4c8d0cc03530ccdd (patch) | |
| tree | 845364c9df4b4db813f910a66487533c12993ca9 /interp | |
| parent | 9b02ddf179b375cb09966b70dd3b119eda0d92c1 (diff) | |
Removing ad-hoc interpretation rules for tactic notations and their genarg.
Now that types can share the same dynamic representation, we do not have
to transtype the topelvel values dynamically and just take advantage of
the standard interpretation function.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrarg.ml | 8 | ||||
| -rw-r--r-- | interp/stdarg.ml | 4 |
2 files changed, 7 insertions, 5 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 84b056ab68..ab54b61977 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -22,7 +22,8 @@ let loc_of_or_by_notation f = function let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type = Obj.magic t -let wit_int_or_var = unsafe_of_type IntOrVarArgType +let wit_int_or_var = + Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "int_or_var" let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type = Genarg.make0 None "intropattern" @@ -43,7 +44,8 @@ let wit_sort : (glob_sort, glob_sort, sorts) genarg_type = let wit_constr = unsafe_of_type ConstrArgType -let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType +let wit_constr_may_eval = + Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval" let wit_uconstr = Genarg.make0 None "uconstr" @@ -64,11 +66,13 @@ let wit_clause_dft_concl = (** Register location *) let () = + register_name0 wit_int_or_var "Constrarg.wit_int_or_var"; register_name0 wit_ref "Constrarg.wit_ref"; register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"; register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; register_name0 wit_uconstr "Constrarg.wit_uconstr"; + register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval"; register_name0 wit_red_expr "Constrarg.wit_red_expr"; register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl"; register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp"; diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 5cfe3854a9..e155a5217d 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -15,9 +15,7 @@ let wit_bool : bool uniform_genarg_type = make0 None "bool" let wit_int : int uniform_genarg_type = - make0 ~dyn:(val_tag (Obj.magic IntOrVarArgType)) None "int" -(** FIXME: IntOrVarArgType is hardwired, but that definition should be the other - way around. *) + make0 None "int" let wit_string : string uniform_genarg_type = make0 None "string" |