diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-11 13:51:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-11 13:51:20 +0000 |
| commit | c4d6bd430c4ba0cbc0c9d444583c8291537ebc3e (patch) | |
| tree | 88defd33087af2ef582aec2b4cc2a4936b60281a /pretyping | |
| parent | 3edd665893c2abfa6e687a7276a17273617dcdd5 (diff) | |
Bug environnement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1242 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 919342585..428af0a4a 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -119,7 +119,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj = then let (x,v1,v2) = destLambda v' in let env1 = push_rel_assum (x,v1) env in - let h2 = inh_conv_coerce_to_fail env isevars u2 + let h2 = inh_conv_coerce_to_fail env1 isevars u2 {uj_val = v2; uj_type = t2 } in fst (abs_rel env !isevars x v1 h2) else @@ -131,7 +131,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj = inh_conv_coerce_to_fail env isevars t1 {uj_val = mkRel 1; uj_type = u1 } in - let h2 = inh_conv_coerce_to_fail env isevars u2 + let h2 = inh_conv_coerce_to_fail env1 isevars u2 { uj_val = mkApp (lift 1 v, [|h1.uj_val|]); uj_type = subst1 h1.uj_val t2 } in |