Exporting the full pretyper options in Goal.constr_of_raw.

2 files changed, 9 insertions, 16 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 43d7b3579e..c660f403fb 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -232,27 +232,20 @@ module Refinable = struct
        many things to go wrong. *)
     handle := fusion delta_list !handle
 
-  (* [constr_of_raw] is a pretyping function. The [check_type] argument
-      asks whether the term should have the same type as the conclusion.
-      [resolve_classes] is a flag on pretyping functions which, if set to true,
-      calls the typeclass resolver.
+  (* [constr_of_raw h tycon flags] is a pretyping function.
+      The [tycon] argument allows to put a type constraint on the returned term.
+      The [flags] argument is passed to the pretyper.
       The principal argument is a [glob_constr] which is then pretyped in the
       context of a term, the remaining evars are registered to the handle.
       It is the main component of the toplevel refine tactic.*)
   (* spiwack: it is not entirely satisfactory to have this function here. Plus it is
       a bit hackish. However it does not seem possible to move it out until
       pretyping is defined as some proof procedure. *)
-  let constr_of_raw handle check_type resolve_classes lvar rawc = (); fun env rdefs gl info ->
+  let constr_of_raw handle tycon flags lvar rawc = (); fun env rdefs gl info ->
     (* We need to keep trace of what [rdefs] was originally*)
     let init_defs = !rdefs in
-    (* if [check_type] is true, then creates a type constraint for the
-       proof-to-be *)
-    let tycon = if check_type then Pretyping.OfType (Evd.evar_concl info) else Pretyping.WithoutTypeConstraint in
     (* call to [understand_tcc_evars] returns a constr with undefined evars
        these evars will be our new goals *)
-    let flags =
-      if resolve_classes then Pretyping.all_no_fail_flags
-      else Pretyping.no_classes_no_fail_inference_flags in
     let (sigma, open_constr) =
       Pretyping.understand_ltac flags !rdefs env lvar tycon rawc
     in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 013b3199a3..db864b273f 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -86,14 +86,14 @@ module Refinable : sig
   val resolve_typeclasses : ?filter:Typeclasses.evar_filter -> ?split:bool -> ?fail:bool -> unit -> unit sensitive
 
 
-  (* [constr_of_raw h check_type resolve_classes] is a pretyping function.
-      The [check_type] argument asks whether the term should have the same
-      type as the conclusion. [resolve_classes] is a flag on pretyping functions
-      which, if set to true, calls the typeclass resolver.
+  (* [constr_of_raw h tycon flags] is a pretyping function.
+      The [tycon] argument allows to put a type constraint on the returned term.
+      The [flags] argument is passed to the pretyper.
       The principal argument is a [glob_constr] which is then pretyped in the
       context of a term, the remaining evars are registered to the handle.
       It is the main component of the toplevel refine tactic.*)
-  val constr_of_raw : handle -> bool -> bool -> Pretyping.ltac_var_map ->
+  val constr_of_raw : handle -> Pretyping.typing_constraint ->
+    Pretyping.inference_flags -> Pretyping.ltac_var_map ->
     Glob_term.glob_constr -> Term.constr sensitive
 
   (* [constr_of_open_constr h check_type] transforms an open constr into a