From 6058cdf5e70822e4501c61dfd969e4746c01145b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 8 Jan 2014 09:06:58 +0100 Subject: Exporting the full pretyper options in Goal.constr_of_raw. --- proofs/goal.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'proofs/goal.mli') diff --git a/proofs/goal.mli b/proofs/goal.mli index 013b3199a..db864b273 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 -- cgit v1.2.3