Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous and current version work).

Changed the type of typing constraints so as to have all the necessary information on abstract tycons.
Updates of subtac to use the new type.



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

5 files changed, 58 insertions, 56 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ec1246b745..4ad85af9a8 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -352,7 +352,7 @@ let find_tomatch_tycon isevars env loc = function
   | Some (_,ind,_),_ 
   (* Otherwise try to get constraints from (the 1st) constructor in clauses *)
   | None, Some (_,(ind,_)) ->
-      Some (0, inductive_template isevars env loc ind)
+      mk_tycon (inductive_template isevars env loc ind)
   | None, None -> 
       empty_tycon
 
@@ -412,7 +412,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
 		current
 	      else
 		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
-		  pb.isevars (make_judge current typ) (0, indt)).uj_val in
+		  pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in
 	    let sigma = Evd.evars_of !(pb.isevars) in
 	    let typ = IsInd (indt,find_rectype pb.env sigma indt) in
 	    ((current,typ),deps))
@@ -1663,7 +1663,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
   (* No type annotation *)
   | None ->
       (match tycon with
-       | Some (0, t) ->
+       | Some (None, t) ->
 	   let names,pred = 
 	     prepare_predicate_from_tycon loc false env isevars tomatchs t 
 	   in Some (build_initial_predicate false names pred)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 841e6b0347..b1b02ffd01 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -160,13 +160,6 @@ module Default = struct
       with Reduction.NotConvertible -> raise NoCoercion
   open Pp
   let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
-(*     (try *)
-(*        msgnl (str "inh_conv_coerces_to_fail called for " ++ *)
-(* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
-(* 	      Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *)
-(* 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
-(* 	      Termops.print_env env); *)
-(*      with _ -> ()); *)
     try (the_conv_x_leq env t c1 isevars, v, t)
     with Reduction.NotConvertible ->
       (try 
@@ -225,18 +218,20 @@ module Default = struct
 	
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to loc env isevars cj (n, t) =
-    if n = 0 then
-      let (evd', val', type') = 
-	try 
-	  inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
-	with NoCoercion ->
-	  let sigma = evars_of isevars in
-	    error_actual_type_loc loc env sigma cj t
-      in
-      let val' = match val' with Some v -> v | None -> assert(false) in
-	(evd',{ uj_val = val'; uj_type = t })
-    else
-      (isevars, cj)
+    match n with
+	None ->
+	  let (evd', val', type') = 
+	    try 
+	      inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
+	    with NoCoercion ->
+	      let sigma = evars_of isevars in
+		error_actual_type_loc loc env sigma cj t
+	  in
+	  let val' = match val' with Some v -> v | None -> assert(false) in
+	    (evd',{ uj_val = val'; uj_type = t })
+      | Some (init, cur) -> (isevars, cj)
+      
+      
 
   open Pp
   let inh_conv_coerces_to loc env isevars t (abs, t') = isevars
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e9f605ecb5..79e25a5afc 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -556,7 +556,7 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 
 (* Operations on value/type constraints *)
 
-type type_constraint_type = int * constr
+type type_constraint_type = (int * int) option * constr
 type type_constraint = type_constraint_type option
 
 type val_constraint = constr option
@@ -578,8 +578,9 @@ type val_constraint = constr option
 (* The empty type constraint *)
 let empty_tycon = None
 
-let mk_tycon_type c = (0, c)
-let mk_abstr_tycon_type n c = (n, c)
+let mk_tycon_type c = (None, c)
+let mk_abstr_tycon_type n c = (Some (n, n), c) (* First component is initial abstraction, second
+						  is current abstraction *)
 
 (* Builds a type constraint *)
 let mk_tycon ty = Some (mk_tycon_type ty)
@@ -651,28 +652,35 @@ let split_tycon loc env isevars tycon =
     match tycon with
       | None -> isevars,(Anonymous,None,None)
       | Some (abs, c) ->
-	  if abs = 0 then real_split c
-	  else if abs = 1 then 
-		isevars, (Anonymous, None, mk_tycon c)
-	      else
-		isevars, (Anonymous, None, Some (pred abs, c))
+	  (match abs with
+	       None -> real_split c
+	     | Some (init, cur) ->
+	       if cur = 1 then isevars, (Anonymous, None, 
+					 Some (Some (init, 0), c))
+	       else
+		 isevars, (Anonymous, None, Some (Some (init, pred cur), c)))
 
 let valcon_of_tycon x = 
   match x with
-    | Some (0, t) -> Some t
+    | Some (None, t) -> Some t
     | _ -> None
 	
-let lift_tycon_type n (abs, c) = 
-  let abs' = abs + n in 
-    if abs' < 0 then raise (Invalid_argument "lift_tycon_type")
-    else (abs', c)
+let lift_tycon_type n (abs, t) =
+  abs, lift n t
+(*  match abs with 
+      None -> (abs, lift n t)
+    | Some (init, abs) ->
+	let abs' = abs + n in 
+	  if abs' < 0 then raise (Invalid_argument "lift_tycon_type")
+	  else (Some (init, abs'), lift n t)*)
 
 let lift_tycon n = option_app (lift_tycon_type n)
 
 let pr_tycon_type env (abs, t) =
-  if abs = 0 then Termops.print_constr_env env t
-  else str "Abstract " ++ int abs ++ str " " ++ Termops.print_constr_env env t
-
+  match abs with 
+      None -> Termops.print_constr_env env t
+    | Some (init, cur) -> str "Abstract (" ++ int init ++ str ","  ++ int cur ++ str ") " ++ Termops.print_constr_env env t
+	
 let pr_tycon env = function
     None -> str "None"
   | Some t -> pr_tycon_type env t
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7260b5ad35..8c5fe9c99b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -87,7 +87,7 @@ val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
 
 val judge_of_new_Type : unit -> unsafe_judgment
 
-type type_constraint_type = int * constr
+type type_constraint_type = (int * int) option * constr
 type type_constraint = type_constraint_type option
 
 type val_constraint = constr option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 217a9714be..b3590492ab 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -259,14 +259,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
   (* in environment [env], with existential variables [(evars_of isevars)] and *)
   (* the type constraint tycon *)
-  let rec pretype (tycon : type_constraint) env isevars lvar c =
-(*    (try 
-       msgnl (str "pretype with tycon: " ++
-	      Evarutil.pr_tycon env tycon ++ str " with evars: " ++ spc () ++
-	      Evd.pr_evar_defs !isevars ++ str " in env: " ++ spc () ++
-	      Termops.print_env env);
-     with _ -> ());*)
-    match c with
+  let rec pretype (tycon : type_constraint) env isevars lvar = function
     | RRef (loc,ref) ->
 	inh_conv_coerce_to_tycon loc env isevars
 	  (pretype_ref isevars env ref)
@@ -294,7 +287,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | RHole (loc,k) ->
 	let ty =
           match tycon with 
-            | Some (n, ty) when n = 0 -> ty
+            | Some (None, ty) -> ty
             | None | Some _ ->
 		e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
 	  { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
@@ -357,9 +350,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let ftycon = 
 	  match tycon with
 	      None -> None
-	    | Some (n, ty) ->
-		if n = 0 then mk_abstr_tycon length ty
-		else Some (n + length, ty)
+	    | Some (None, ty) -> mk_abstr_tycon length ty
+	    | Some (Some (init, cur), ty) ->
+		Some (Some (length + init, cur), ty)
 	in
 	let fj = pretype ftycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
@@ -375,11 +368,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 		      let typ' = nf_isevar !isevars typ in
 		      let tycon = 
-			match tycon with
+			match tycon with			    
 			    Some (abs, ty) ->
-			      isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-			      (abs, ty);			      
-			      Some (pred abs, nf_isevar !isevars ty)
+			      (match abs with
+				   None ->
+				     isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
+				       (abs, ty);
+				     Some (None, nf_isevar !isevars ty)
+				 | Some (init, cur) ->
+				     isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
+				       (abs, ty);
+				     Some (Some (init, pred cur), nf_isevar !isevars ty))
 			  | None -> None
 		      in 
 			apply_rec env (n+1) 
@@ -532,7 +531,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  jtyp.uj_val, jtyp.uj_type
 	    | None -> 
 		let p = match tycon with
-		  | Some (n, ty) when n = 0 -> ty
+		  | Some (None, ty) -> ty
 		  | None | Some _ ->
                       e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
 		in