diff options
| author | herbelin | 2011-12-18 23:56:06 +0000 |
|---|---|---|
| committer | herbelin | 2011-12-18 23:56:06 +0000 |
| commit | dadfbd96378d4c1b794ffc341bd10cc4d63b225d (patch) | |
| tree | 7ff1c2d295f7ff831302b92de6f00f686d0c9f3b /pretyping/tacred.mli | |
| parent | 5536b6d56226c4e53bbd6c5ae9a2c419c6f08874 (diff) | |
Granted legitimate wish #2607 (not exposing crude fixpoint body of
unfolded fixpoints when calling destruct). However, this might break
compatibility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/tacred.mli')
| -rw-r--r-- | pretyping/tacred.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index f0f5f66d31..8fd14dccbc 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -99,5 +99,8 @@ val reduce_to_quantified_ref : val reduce_to_atomic_ref : env -> evar_map -> global_reference -> types -> types +val find_hnf_rectype : + env -> evar_map -> types -> inductive * constr list + val contextually : bool -> occurrences * constr_pattern -> (patvar_map -> reduction_function) -> reduction_function |