diff options
| author | Hugo Herbelin | 2017-05-01 19:40:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 01:58:11 +0200 |
| commit | a3407e27e60104fa8ea2e62433f9920a41a22757 (patch) | |
| tree | 032bbe79237163eb7d914323717edb26a16075e1 /plugins | |
| parent | bcc9165aec1a80d563d7060ef127ad022e9ed008 (diff) | |
Splitting interp_open_constr into two variants, with or without type classes.
This simplifies the API as before, inference of instances of type
classes was iff a type constraint was given.
We then export these both versions of interp_open_constr.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 8 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 8 |
2 files changed, 12 insertions, 4 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a9ec779d11..b105074e82 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -673,10 +673,10 @@ let pure_open_constr_flags = { (* Interprets an open constr *) let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c = - let flags = - if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags () - else open_constr_use_classes_flags () in - interp_gen expected_type ist false flags env sigma c + interp_gen expected_type ist false (open_constr_no_classes_flags ()) env sigma c + +let interp_open_constr_with_classes ?(expected_type=WithoutTypeConstraint) ist env sigma c = + interp_gen expected_type ist false (open_constr_use_classes_flags ()) env sigma c let interp_pure_open_constr ist = interp_gen WithoutTypeConstraint ist false pure_open_constr_flags diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 2ec45312ea..c80b1738f8 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -78,6 +78,14 @@ val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr bindings -> Evd.evar_map * constr bindings +val interp_open_constr : ?expected_type:Pretyping.typing_constraint -> + interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr -> Evd.evar_map * EConstr.constr + +val interp_open_constr_with_classes : ?expected_type:Pretyping.typing_constraint -> + interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr -> Evd.evar_map * EConstr.constr + val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr with_bindings -> Evd.evar_map * EConstr.constr with_bindings |