diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-26 14:29:40 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-26 14:29:40 +0000 |
| commit | 517f47037053c873f715428795d2199459b9924b (patch) | |
| tree | d55df810f8b5c74a23c6159320f166bb66aba8de /pretyping/evarutil.mli | |
| parent | ecf8f5a0a7dd1a2f46d20df1680a4554d99d18b0 (diff) | |
Fixing Derive Inversion for new proof engine
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13027 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index cbdc20f92..e21516681 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -198,3 +198,5 @@ val clear_hyps_in_evi : evar_map ref -> named_context_val -> types -> val push_rel_context_to_named_context : Environ.env -> types -> named_context_val * types * constr list + +val generalize_evar_over_rels : evar_map -> existential -> types * constr list |