diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-19 01:06:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-19 01:07:31 +0200 |
| commit | 56ece74efc25af1b0e09265f3c7fcf74323abcaf (patch) | |
| tree | 56d854b6484ffc8525b4203b57a1d344e91b9940 /proofs/goal.mli | |
| parent | e171b71ffa0949ca21c12d79773a6aa9b64c439e (diff) | |
Removing a use of Goal.refine.
Diffstat (limited to 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index 696c91dc5..988853382 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -87,16 +87,6 @@ module Refinable : sig val resolve_typeclasses : ?filter:Typeclasses.evar_filter -> ?split:bool -> ?fail:bool -> unit -> unit sensitive - (* [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 -> 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 goal-sensitive constr, adding the undefined variables to the set of subgoals. If [check_type] is true, the term is coerced to the conclusion of the goal. |