diff options
author | 2001-11-20 15:44:51 +0000 | |
---|---|---|
committer | 2001-11-20 15:44:51 +0000 | |
commit | 6a30d4b83ee39f98847ef6ed0e015db65872b88d (patch) | |
tree | ad329fbfdececbb504591e6745d28488b5b7952f | |
parent | 72c03f36e2e969992acf8e0398bbf7ae2c2c70b8 (diff) |
Bug mauvaise instance
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2212 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | pretyping/evarutil.ml | 12 |
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 |