The "clean integration of subtac" patch.

Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive).
The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed.
The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have 
a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready
for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml.
Subtac is now working as well as I demonstrated at TYPES.



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

7 files changed, 47 insertions, 41 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7a77d6eab..b3cff232b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1482,7 +1482,7 @@ let set_arity_signature dep n arsign tomatchl pred x =
   in
   decomp_block [] pred (tomatchl,arsign)
 
-let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
+let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
   let cook (n, l, env, signs) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
 	let indf' = lift_inductive_family n indf in
@@ -1594,7 +1594,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       (match tycon with
        | Some (None, t) ->
 	   let names,pred = 
-	     prepare_predicate_from_tycon loc false env isevars tomatchs t 
+	     prepare_predicate_from_tycon loc false env isevars tomatchs sign t 
 	   in Some (build_initial_predicate false names pred)
        | _ -> None)
 
@@ -1607,7 +1607,8 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
       let _ = 
 	option_map (fun tycon -> 
-		      isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val tycon)
+		      isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val 
+		      (lift_tycon_type (List.length arsign) tycon))
 	  tycon
       in
       let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 1b128e43a..8a55a46d2 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -35,6 +35,12 @@ module type S = sig
      type a sort; it fails if no coercion is applicable *)
   val inh_coerce_to_sort : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
+
+  (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
+     inserts a coercion into [j], if needed, in such a way it gets as
+     type its base type (the notion depends on the coercion system) *)
+  val inh_coerce_to_base : loc ->
+    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
   (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
@@ -143,6 +149,8 @@ module Default = struct
 	| _ ->
 	    inh_tosort_force loc env isevars j
 
+  let inh_coerce_to_base loc env isevars j = (isevars, j)
+
   let inh_coerce_to_fail env isevars c1 v t =
     let v', t' =
       try 
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 667f20730..5476a4820 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -33,13 +33,19 @@ module type S = sig
      type a sort; it fails if no coercion is applicable *)
   val inh_coerce_to_sort : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
+
+  (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
+     inserts a coercion into [j], if needed, in such a way it gets as
+     type its base type (the notion depends on the coercion system) *)
+  val inh_coerce_to_base : loc ->
+    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
   (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
   val inh_conv_coerce_to : loc -> 
     env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
-
+    
   (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
      is coercible to an object of type [t'] adding evar constraints if needed;
      it fails if no coercion exists *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ec6edcbdf..1fcc6d8b7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -374,7 +374,7 @@ let rec detype isgoal avoid env t =
 	  RVar (dl, id))
     | Sort s -> RSort (dl,detype_sort s)
     | Cast (c1,k,c2) ->
-	RCast(dl,detype isgoal avoid env c1, k,
+	RCast(dl,detype isgoal avoid env c1, CastConv k,
               detype isgoal avoid env c2)
     | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
     | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d1d30980b..be24d22b5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -363,17 +363,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
 
     | RApp (loc,f,args) -> 
-	let length = List.length args in	 
-	let ftycon = 
-	  match tycon with
-	      None -> None
-	    | Some (None, ty) -> mk_abstr_tycon length ty
-	    | Some (Some (init, cur), ty) ->
-		Some (Some (length + init, length + cur), ty)
-	in
 	let fj = pretype empty_tycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
-	let rec apply_rec env n resj tycon = function
+	let rec apply_rec env n resj = function
 	  | [] -> resj
 	  | c::rest ->
 	      let argloc = loc_of_rawconstr c in
@@ -384,33 +376,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		      let hj = pretype (mk_tycon c1) env isevars lvar c in
 		      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 = 
-			option_map 
-			  (fun (abs, ty) ->
-			     match abs with
-				 None ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
-				     (abs, ty);
-				   (abs, ty)
-			       | Some (init, cur) ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-				     (abs, ty);
-				   (Some (init, pred cur), ty))
-			  tycon
-		      in 
 			apply_rec env (n+1) 
 			  { uj_val = nf_isevar !isevars value;
-			    uj_type = nf_isevar !isevars typ' }
-			  (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest
-
+			    uj_type = typ' }
+			  rest
 		  | _ ->
 		      let hj = pretype empty_tycon env isevars lvar c in
 			error_cant_apply_not_functional_loc 
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let ftycon = option_map (lift_abstr_tycon_type (-1)) ftycon in
-	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
+	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in
 	let resj =
 	  match kind_of_term resj.uj_val with
 	  | App (f,args) when isInd f ->
@@ -590,12 +566,19 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  tycon env (* loc *) (po,tml,eqns)
 
     | RCast(loc,c,k,t) ->
-	let tj = pretype_type empty_valcon env isevars lvar t in
-	let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
-	  (* User Casts are for helping pretyping, experimentally not to be kept*)
-	  (* ... except for Correctness *)
-	let v = mkCast (cj.uj_val, k, tj.utj_val) in
-	let cj = { uj_val = v; uj_type = tj.utj_val } in
+	let cj =
+	  match k with
+	      CastCoerce ->
+		let cj = pretype empty_tycon env isevars lvar c in
+		  evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj
+	    | CastConv k ->
+		let tj = pretype_type empty_valcon env isevars lvar t in
+		let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
+		  (* User Casts are for helping pretyping, experimentally not to be kept*)
+		  (* ... except for Correctness *)
+		let v = mkCast (cj.uj_val, k, tj.utj_val) in
+		  { uj_val = v; uj_type = tj.utj_val }
+	in
 	  inh_conv_coerce_to_tycon loc env isevars cj tycon
 
     | RDynamic (loc,d) ->
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index d536adcb0..480ee13b2 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -47,6 +47,10 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
+type cast_type =
+  | CastConv of cast_kind
+  | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
+
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -64,7 +68,7 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * hole_kind)
-  | RCast of loc * rawconstr * cast_kind * rawconstr
+  | RCast of loc * rawconstr * cast_type * rawconstr
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d85ca0158..d64ba03a7 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -44,6 +44,10 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
+type cast_type =
+  | CastConv of cast_kind
+  | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
+
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -61,7 +65,7 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * Evd.hole_kind)
-  | RCast of loc * rawconstr * cast_kind * rawconstr
+  | RCast of loc * rawconstr * cast_type * rawconstr
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr