diff options
| author | xclerc | 2013-12-02 13:09:42 +0100 |
|---|---|---|
| committer | xclerc | 2013-12-02 13:09:42 +0100 |
| commit | 76d4622212e7c5596eb03fd17ff0177b6c44a990 (patch) | |
| tree | 480237faebb6b2dae88f0c157c4307109105aec7 /interp | |
| parent | c101a710c96e03e228e4b1aacee8edebd3c8dabf (diff) | |
| parent | cb290d81c46ec370e303e1414e203c40c8fa1174 (diff) | |
Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr//gitroot/coq/coq into trunk
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrarg.ml | 9 | ||||
| -rw-r--r-- | interp/constrarg.mli | 4 |
2 files changed, 3 insertions, 10 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 16af7c3080..4f20dd5606 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -47,7 +47,7 @@ let wit_pattern_ident = wit_ident_gen false let wit_var = unsafe_of_type VarArgType -let wit_ref = unsafe_of_type RefArgType +let wit_ref = Genarg.make0 None "ref" let wit_quant_hyp = unsafe_of_type QuantHypArgType @@ -60,11 +60,7 @@ let wit_constr = unsafe_of_type ConstrArgType let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType -let wit_open_constr_gen b = unsafe_of_type (OpenConstrArgType b) - -let wit_open_constr = wit_open_constr_gen false - -let wit_casted_open_constr = wit_open_constr_gen true +let wit_open_constr = unsafe_of_type OpenConstrArgType let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType @@ -75,6 +71,7 @@ let wit_red_expr = unsafe_of_type RedExprArgType (** Register location *) let () = + 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"; diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 1233e165fd..b83c20065d 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -57,12 +57,8 @@ val wit_constr_may_eval : (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval, constr) genarg_type -val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type - val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type -val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type - val wit_constr_with_bindings : (constr_expr with_bindings, glob_constr_and_expr with_bindings, |