Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.

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

1 files changed, 5 insertions, 8 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c7258ccfe..2de53489d 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1504,6 +1504,10 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
    constraint on its domain and codomain. If the input constraint is
    an evar instantiate it with the product of 2 new evars. *)
 
+let unlift_tycon init cur c =
+  if cur = 1 then None, c
+  else Some (init, pred cur), c
+
 let split_tycon loc env evd tycon =
   let rec real_split evd c =
     let t = whd_betadeltaiota env evd c in
@@ -1523,14 +1527,7 @@ let split_tycon loc env evd tycon =
 		 let evd', (n, dom, rng) = real_split evd c in
 		   evd', (n, mk_tycon dom, mk_tycon rng)
 	     | Some (init, cur) ->
-		 if cur = 0 then
-		   let evd', (x, dom, rng) = real_split evd c in
-		     evd, (Anonymous,
-			  Some (None, dom),
-			  Some (None, rng))
-		 else
-		   evd, (Anonymous, None,
-			Some (if cur = 1 then None,c else Some (init, pred cur), c)))
+		 evd, (Anonymous, None, Some (unlift_tycon init cur c)))
 
 let valcon_of_tycon x =
   match x with