Bug mauvaise instance

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2212 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 5 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b08286ef3..a56e87b2e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -162,12 +162,14 @@ let split_evar_to_arrow sigma (ev,args) =
   let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in
   let newenv = push_named_decl (nvar, None, dom) evenv in
   let (sigma2,rng) = new_type_var newenv sigma1 in
-  let prod = mkProd (named_hd newenv dom Anonymous, dom, subst_var nvar rng) in
+  let x = named_hd newenv dom Anonymous in
+  let prod = mkProd (x, dom, subst_var nvar rng) in
   let sigma3 = Evd.define sigma2 ev prod in
-  let dsp = fst (destEvar dom) in
-  let rsp = fst (destEvar rng) in
-  (sigma3, prod,
-   (dsp,args), (rsp, array_cons (mkRel 1) (Array.map (lift 1) args)))
+  let evdom = fst (destEvar dom), args in
+  let evrng =
+    fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
+  let prod' = mkProd (x, mkEvar evdom, mkEvar evrng) in
+  (sigma3, prod', evdom, evrng)
 
 let define_evar_as_arrow sigma ev =
   let (sigma, prod, _, _) = split_evar_to_arrow sigma ev in