diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-08 09:06:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-10 17:46:36 +0100 |
| commit | 6058cdf5e70822e4501c61dfd969e4746c01145b (patch) | |
| tree | 08a86366100937b2f91742807c3ad76ec0848048 /proofs/goal.mli | |
| parent | a6ca35c30199f3ccf0ebb7d9b200190e345c4d50 (diff) | |
Exporting the full pretyper options in Goal.constr_of_raw.
Diffstat (limited to 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 10 |
1 files changed, 5 insertions, 5 deletions
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 |