From a3407e27e60104fa8ea2e62433f9920a41a22757 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 19:40:55 +0200
Subject: 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.
---
 plugins/ltac/tacinterp.ml  | 8 ++++----
 plugins/ltac/tacinterp.mli | 8 ++++++++
 2 files changed, 12 insertions(+), 4 deletions(-)

(limited to 'plugins')

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
 
-- 
cgit v1.2.3