diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-01 16:54:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-01 17:03:31 +0200 |
| commit | 1d6eac66b4f21a768e98d01416e4ecef68ada377 (patch) | |
| tree | 5d90b0187bf12ec89ca3d74988b450c0984e7458 /tactics/taccoerce.mli | |
| parent | a4d454beaafd030a5564a395d380748cf90e1b75 (diff) | |
Moving the decompose tactic out of the AST.
Diffstat (limited to 'tactics/taccoerce.mli')
| -rw-r--r-- | tactics/taccoerce.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index cec25d9bd..c0ede540c 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -82,8 +82,6 @@ val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference -val coerce_to_inductive : Value.t -> inductive - val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis |