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

---
 plugins/subtac/subtac_pretyping_F.ml | 36 +++++++++++++++++++++++++++++-------
 1 file changed, 29 insertions(+), 7 deletions(-)

(limited to 'plugins/subtac/subtac_pretyping_F.ml')

diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 16f2031b..7fcd4267 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: subtac_pretyping_F.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -166,6 +166,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 *)
@@ -233,7 +255,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let newenv =
 	  let marked_ftys =
 	    Array.map (fun ty -> let sort = Retyping.get_type_of env !evdref ty in
-				   mkApp (Lazy.force Subtac_utils.fix_proto, [| sort; ty |]))
+			 mkApp (delayed_force Subtac_utils.fix_proto, [| sort; ty |]))
 	      ftys
 	  in
 	    push_rec_types (names,marked_ftys,[||]) env
@@ -355,7 +377,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
@@ -586,11 +608,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  (pretype tycon env evdref lvar c).uj_val
       | IsType ->
 	  (pretype_type empty_valcon env evdref lvar c).utj_val in
-    evdref := fst (consider_remaining_unif_problems env !evdref);
+    evdref := consider_remaining_unif_problems env !evdref;
     if resolve_classes then
-      evdref :=
-        Typeclasses.resolve_typeclasses ~onlyargs:false
+      (evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
 	  ~split:true ~fail:fail_evar env !evdref;
+       evdref := consider_remaining_unif_problems env !evdref);
     let c = if expand_evar then nf_evar !evdref c' else c' in
     if fail_evar then check_evars env Evd.empty !evdref c;
     c
@@ -603,7 +625,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let understand_judgment sigma env c =
     let evdref = ref (create_evar_defs sigma) in
     let j = pretype empty_tycon env evdref ([],[]) c in
-    let evd,_ = consider_remaining_unif_problems env !evdref in
+    let evd = consider_remaining_unif_problems env !evdref in
     let j = j_nf_evar evd j in
     check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
     j
-- 
cgit v1.2.3