From e32113e515796b821b072a0b028b573f9ff05041 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Mar 2000 00:04:06 +0000
Subject: Inlining prod_create

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@336 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 77366d6015..0524a78473 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -38,7 +38,6 @@ let filter_sign p sign x =
     (x,[],nil_sign)
 
 
-
 (*------------------------------------*
  * functional operations on evar sets *
  *------------------------------------*)
@@ -74,8 +73,10 @@ let split_evar_to_arrow sigma c =
   let nvar = next_ident_away (id_of_string "x") (ids_of_sign hyps) in
   let nevenv = push_var (nvar,dom) evenv in
   let (sigma2,rng) = new_type_var nevenv sigma1 in
-  let prod = prod_create nevenv (incast_type dom, 
-				 subst_var nvar (body_of_type rng)) in
+  let prod =
+    let a = incast_type dom in
+    mkProd (named_hd nevenv a Anonymous) a (subst_var nvar (body_of_type rng))
+  in
   let sigma3 = Evd.define sigma2 ev prod in
   let dsp = num_of_evar (body_of_type dom) in
   let rsp = num_of_evar (body_of_type rng) in
-- 
cgit v1.2.3