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/ltac/tacinterp.ml | |
| 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/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 8 |
1 files changed, 4 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 |