Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->

splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added
shortcuts for "fst (decompose_prod t)" and co.




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

5 files changed, 8 insertions, 8 deletions

diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index f45efe50b9..3e80be65ef 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -812,7 +812,7 @@ let rec unify_clauses k pv =
 let abstract_conclusion typ cs =
   let n = List.length (assums_of_rel_context cs.cs_args) in
   let (sign,p) = decompose_prod_n n typ in
-  lam_it p sign
+  it_mkLambda p sign
 
 let infer_predicate loc env isevars typs cstrs indf =
   (* Il faudra substituer les isevars a un certain moment *)
@@ -1911,7 +1911,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 		      let previd, id = 
 			let name = 
 			  match kind_of_term arg with 
-			      Rel n -> pi1 (lookup_rel n (rel_context env))
+			      Rel n -> pi1 (lookup_rel n env)
 			    | _ -> name
 			in
 			  make_prime avoid name 
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 510229ae6f..cbfec12df4 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -116,7 +116,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   let k, ctx', imps, subst = 
     let c = Command.generalize_constr_expr tclass ctx in
     let c', imps = interp_type_evars_impls ~evdref:isevars env c in
-    let ctx, c = Sign.decompose_prod_assum c' in
+    let ctx, c = decompose_prod_assum c' in
     let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
       cl, ctx, imps, (List.rev args)
   in
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 519626a3a3..0af732f858 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -119,7 +119,7 @@ module Coercion = struct
     and coerce' env x y : (Term.constr -> Term.constr) option =
       let subco () = subset_coerce env isevars x y in
       let dest_prod c =
-	match Reductionops.decomp_n_prod env (evars_of !isevars) 1 c with
+	match Reductionops.splay_prod_n env (evars_of !isevars) 1 c with
 	| [(na,b,t)], c -> (na,t), c
 	| _ -> raise NoSubtacCoercion
       in
@@ -484,7 +484,7 @@ module Coercion = struct
 	| Some (init, cur) -> init, cur
     in
       try 
-	let rels, rng = Reductionops.decomp_n_prod env (evars_of isevars) nabs t in
+	let rels, rng = Reductionops.splay_prod_n env (evars_of isevars) nabs t in
 	(* The final range free variables must have been replaced by evars, we accept only that evars
 	   in rng are applied to free vars. *)
 	if noccur_with_meta 1 (succ nabs) rng then (
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index cc1e2dde2f..839597ece8 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -226,7 +226,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
          doesn't seem to worth the effort (except for huge mutual 
 	 fixpoints ?) *)
       let m = Term.nb_prod fixtype in
-      let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
+      let ctx = fst (decompose_prod_n_assum m fixtype) in
 	list_map_i (fun i _ -> i) 0 ctx
 
 let reduce_fix =
@@ -238,7 +238,7 @@ let declare_mutual_definition l =
     list_split3
       (List.map (fun x -> 
 	let subs, typ = (subst_body false x) in
-	  snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
+	  (strip_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
   in
 (*   let fixdefs = List.map reduce_fix fixdefs in *)
   let fixkind = Option.get (List.hd l).prg_fixkind in
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 8201e8fdcc..023213ecbc 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -144,7 +144,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     let s' = mkProd (Anonymous, ind, s) in
     let ccl = lift 1 (decomp n pj.uj_val) in
     let ccl' = mkLambda (Anonymous, ind, ccl) in
-      {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} 
+      {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign} 
 
   (*************************************************************************)
   (* Main pretyping function                                               *)