diff options
| author | herbelin | 2012-07-29 05:14:44 +0000 |
|---|---|---|
| committer | herbelin | 2012-07-29 05:14:44 +0000 |
| commit | c6763b44c75b2bd9aebdbcd0798287c90431cde4 (patch) | |
| tree | 5a04663d2ef32d34fc239a3923a26c6e2ca3d7f0 /pretyping/evarutil.ml | |
| parent | 254da5d698f821172c70899c6a1d95b3b15f8cd8 (diff) | |
Fixing #2836 (materialize_evar might refine as a side effect the
current evar to project; this may happen if this evar is dependent and
is involved in evar-evar conversion problem eventually solved by
instantiating the current evar; could maybe be optimized when the evar
to materialize has invertible instance in which case
define_evar_from_virtual_equation applied on the current evar could be
shortcut, avoiding to create an evar).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15657 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 036bed5252..a2c63982bc 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -146,6 +146,11 @@ let noccur_evar evd evk c = in try occur_rec c; true with Occur -> false +let normalize_evar evd ev = + match kind_of_term (whd_evar evd (mkEvar ev)) with + | Evar (evk,args) -> (evk,args) + | _ -> assert false + (**********************) (* Creating new metas *) (**********************) @@ -1591,6 +1596,8 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = let ty = get_type_of env' !evdref t in let (evd,evar'',ev'') = materialize_evar (evar_define conv_algo) env' !evdref k ev ty in + (* materialize_evar may instantiate ev' by another evar; adjust it *) + let (evk',args' as ev') = normalize_evar evd ev' in let evd = (* Try to project (a restriction of) the left evar ... *) try |