diff options
| author | herbelin | 2010-05-26 14:29:40 +0000 |
|---|---|---|
| committer | herbelin | 2010-05-26 14:29:40 +0000 |
| commit | 517f47037053c873f715428795d2199459b9924b (patch) | |
| tree | d55df810f8b5c74a23c6159320f166bb66aba8de /pretyping | |
| 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')
| -rw-r--r-- | pretyping/evarutil.ml | 10 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 2 |
2 files changed, 12 insertions, 0 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 000c062832..f63c01a3ef 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -349,6 +349,16 @@ let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty = evdref := evd'; ev +(* This assumes an evar with identity instance and generalizes it over only + the de Bruijn part of the context *) +let generalize_evar_over_rels sigma (ev,args) = + let evi = Evd.find sigma ev in + let sign = named_context_of_val evi.evar_hyps in + List.fold_left2 + (fun (c,inst as x) a d -> + if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x) + (evi.evar_concl,[]) (Array.to_list args) sign + (*------------------------------------* * operations on the evar constraints * *------------------------------------*) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index cbdc20f92a..e21516681b 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 |