From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 6 Aug 2010 16:15:08 -0400
Subject: Imported Upstream version 8.3~rc1+dfsg

---
 pretyping/vnorm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/vnorm.ml')

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 2de542cd..2c8705d5 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: vnorm.ml 13351 2010-07-29 15:26:31Z barras $ i*)
 
 open Names
 open Declarations
@@ -117,7 +117,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p =
     let carity = snd (rtbl.(i)) in
     let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in
     let codom =
-      let papp = mkApp(p,crealargs) in
+      let papp = mkApp(lift (List.length decl) p,crealargs) in
       if dep then
 	let cstr = ith_constructor_of_inductive ind (i+1) in
         let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
-- 
cgit v1.2.3