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

4 files changed, 39 insertions, 11 deletions

diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 3c907962ce..fe4db0de14 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -493,8 +493,7 @@ module Coercion = struct
 		   with NoCoercion ->
 		     coerce_itf loc env' isevars None t t')
 	    with NoSubtacCoercion ->
-	      let sigma =  isevars in
-		error_cannot_coerce env' sigma (t, t'))
+	      error_cannot_coerce env' isevars (t, t'))
 	else isevars
       with _ -> isevars
 end
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 80527f01d5..524cfd7182 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -164,6 +164,28 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     | RProp c -> judge_of_prop_contents c
     | RType _ -> judge_of_new_Type ()
 
+  let split_tycon_lam loc env evd tycon =
+    let rec real_split evd c =
+      let t = whd_betadeltaiota env evd c in
+	match kind_of_term t with
+	| Prod (na,dom,rng) -> evd, (na, dom, rng)
+	| Evar ev when not (Evd.is_defined_evar evd ev) ->
+	    let (evd',prod) = define_evar_as_product evd ev in
+	    let (_,dom,rng) = destProd prod in
+	      evd',(Anonymous, dom, rng)
+	| _ -> error_not_product_loc loc env evd c
+    in
+      match tycon with
+      | None -> evd,(Anonymous,None,None)
+      | Some (abs, c) ->
+	  (match abs with
+	   | None ->
+	       let evd', (n, dom, rng) = real_split evd c in
+		 evd', (n, mk_tycon dom, mk_tycon rng)
+	   | Some (init, cur) ->
+	       evd, (Anonymous, None, Some (Some (init, succ cur), c)))
+	    
+	    
   (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
   (* in environment [env], with existential variables [( evdref)] and *)
   (* the type constraint tycon *)
@@ -353,7 +375,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  evd, Some ty')
 	  evdref tycon
 	in
-	let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in
+	let (name',dom,rng) = evd_comb1 (split_tycon_lam loc env) evdref tycon' in
 	let dom_valcon = valcon_of_tycon dom in
 	let j = pretype_type dom_valcon env evdref lvar c1 in
 	let var = (name,None,j.utj_val) in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c7258ccfeb..2de53489d8 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
diff --git a/test-suite/bugs/closed/shouldsucceed/2347.v b/test-suite/bugs/closed/shouldsucceed/2347.v
new file mode 100644
index 0000000000..e433f158e4
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2347.v
@@ -0,0 +1,10 @@
+Require Import EquivDec List.
+Generalizable All Variables.
+
+Program Definition list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq := 
+ (fun (x y : list A) => _).
+Admit Obligations of list_eqdec.
+
+Program Definition list_eqdec' `(eqa : EqDec A eq) : EqDec (list A) eq :=
+  (fun _ : nat => (fun (x y : list A) => _)) 0.
+Admit Obligations of list_eqdec'.