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

14 files changed, 28 insertions, 28 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index dcd0ea469c..515d4aa932 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -228,10 +228,10 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   let ci=pred (snd cstr) in
   let branch i=
     let ti=Term.prod_appvect types.(i) argv in
-    let rc=fst (Sign.decompose_prod_assum ti) in
+    let rc=fst (decompose_prod_assum ti) in
     let head=
       if i=ci then special else default in  
-      Sign.it_mkLambda_or_LetIn head rc in
+      it_mkLambda_or_LetIn head rc in
   let branches=Array.init lp branch in
   let casee=mkRel 1 in
   let pred=mkLambda(Anonymous,intype,outtype) in
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index a4d2445ecd..f290fea810 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -773,7 +773,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
    and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
 
 let rec decomp_lams_eta_n n env c t =
-  let rels = fst (decomp_n_prod env none n t) in
+  let rels = fst (splay_prod_n env none n t) in
   let rels = List.map (fun (id,_,c) -> (id,c)) rels in
   let m = nb_lam c in
   if m >= n then decompose_lam_n n c
diff --git a/contrib/firstorder/formula.ml b/contrib/firstorder/formula.ml
index ac32f6abee..0be3a4b399 100644
--- a/contrib/firstorder/formula.ml
+++ b/contrib/firstorder/formula.ml
@@ -57,8 +57,8 @@ let ind_hyps nevar ind largs gls=
   let lp=Array.length types in     
   let myhyps i=
     let t1=Term.prod_applist types.(i) largs in
-    let t2=snd (Sign.decompose_prod_n_assum nevar t1) in
-      fst (Sign.decompose_prod_assum t2) in
+    let t2=snd (decompose_prod_n_assum nevar t1) in
+      fst (decompose_prod_assum t2) in
     Array.init lp myhyps
 
 let special_nf gl=
diff --git a/contrib/firstorder/formula.mli b/contrib/firstorder/formula.mli
index dca55d0bdb..9e9d1e1220 100644
--- a/contrib/firstorder/formula.mli
+++ b/contrib/firstorder/formula.mli
@@ -29,7 +29,7 @@ type counter = bool -> metavariable
 val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array
 
 val ind_hyps : int -> inductive -> constr list -> 
-  Proof_type.goal Tacmach.sigma -> Sign.rel_context array
+  Proof_type.goal Tacmach.sigma -> rel_context array
 
 type atoms = {positive:constr list;negative:constr list}
 
diff --git a/contrib/firstorder/instances.ml b/contrib/firstorder/instances.ml
index 56cea8e075..3e087cd8b6 100644
--- a/contrib/firstorder/instances.ml
+++ b/contrib/firstorder/instances.ml
@@ -133,7 +133,7 @@ let mk_open_instance id gl m t=
     Pretyping.Default.understand evmap env (raux m rawt)
   with _ -> 
     error "Untypable instance, maybe higher-order non-prenex quantification" in
-    Sign.decompose_lam_n_assum m ntt
+    decompose_lam_n_assum m ntt
 
 (* tactics   *)
 
diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml
index 6c00e4eace..91607ec40f 100644
--- a/contrib/firstorder/rules.ml
+++ b/contrib/firstorder/rules.ml
@@ -128,7 +128,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
        let vars=Array.init p (fun j->mkRel (p-j)) in
        let capply=mkApp ((lift p cstr),vars) in
        let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
-	 Sign.it_mkLambda_or_LetIn head rc in
+	 it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
        let newhyps=list_tabulate myterm lp in
 	 tclIFTHENELSE
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 52543cea11..b9b47fde11 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -205,7 +205,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
     
 
 
-let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  = 
+let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  = 
   let nochange ?t' msg  = 
     begin 
       observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t  ++ str "    " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t );
@@ -295,7 +295,7 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  =
     in
     let new_type_of_hyp = Reductionops.nf_betaiota  new_type_of_hyp in 
     let new_ctxt,new_end_of_type = 
-      Sign.decompose_prod_n_assum ctxt_size new_type_of_hyp 
+      decompose_prod_n_assum ctxt_size new_type_of_hyp 
     in 
     let prove_new_hyp : tactic = 
       tclTHEN
@@ -390,7 +390,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
       let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in 
       (* length of context didn't change ? *)
       let new_context,new_typ_of_hyp = 
-	 Sign.decompose_prod_n_assum (List.length context) reduced_type_of_hyp
+	 decompose_prod_n_assum (List.length context) reduced_type_of_hyp
       in
         tclTHENLIST 
 	[
@@ -858,7 +858,7 @@ let build_proof
 
 (* Proof of principles from structural functions *) 
 let is_pte_type t =
-  isSort (snd (decompose_prod t))
+  isSort ((strip_prod t))
     
 let is_pte (_,_,t) = is_pte_type t
 
@@ -948,7 +948,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 (*   observe (str "f_body_with_params_and_other_fun " ++  pr_lconstr f_body_with_params_and_other_fun); *)
   let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
 (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
-  let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) 
+  let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args) 
     (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
   let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in
@@ -1206,7 +1206,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
     in
     let intros_after_fixes : tactic = 
       fun gl -> 
-	let ctxt,pte_app =  (Sign.decompose_prod_assum (pf_concl gl)) in
+	let ctxt,pte_app =  (decompose_prod_assum (pf_concl gl)) in
 	let pte,pte_args = (decompose_app pte_app) in
 	try
 	  let pte = try destVar pte with _ -> anomaly "Property is not a variable"  in 
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 49efe362c8..49d1a179b4 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -63,7 +63,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let env = Global.env () in 
   let env_with_params = Environ.push_rel_context princ_type_info.params env in
   let tbl = Hashtbl.create 792 in
-  let rec change_predicates_names (avoid:identifier list) (predicates:Sign.rel_context)  : Sign.rel_context = 
+  let rec change_predicates_names (avoid:identifier list) (predicates:rel_context)  : rel_context = 
     match predicates with 
     | [] -> []
     |(Name x,v,t)::predicates -> 
@@ -433,7 +433,7 @@ exception Not_Rec
 
 let get_funs_constant mp dp = 
   let rec get_funs_constant const e : (Names.constant*int) array = 
-    match kind_of_term (snd (decompose_lam e)) with 
+    match kind_of_term ((strip_lam e)) with 
       | Fix((_,(na,_,_))) -> 
 	  Array.mapi 
 	    (fun i na -> 
@@ -600,20 +600,20 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
       List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
     let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in 
-    let ctxt,fix = Sign.decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*)
+    let ctxt,fix = decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = destFix fix in 
     let other_result = 
       List.map (* we can now compute the other principles *)
 	(fun scheme_type -> 
 	   incr i;
 	   observe (Printer.pr_lconstr scheme_type);
-	   let type_concl = snd (Sign.decompose_prod_assum scheme_type) in 
+	   let type_concl = (strip_prod_assum scheme_type) in 
 	   let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in 
 	   let f = fst (decompose_app applied_f) in
 	   try (* we search the number of the function in the fix block (name of the function) *)
 	     Array.iteri 
 	     (fun j t -> 
-		let t =  snd (Sign.decompose_prod_assum t) in 
+		let t =  (strip_prod_assum t) in 
 		let applied_g = List.hd (List.rev (snd (decompose_app t))) in 
 		let g = fst (decompose_app applied_g) in
 		if eq_constr f g
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index c09c79c180..a78746d293 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -11,7 +11,7 @@ let is_rec_info scheme_info =
   let test_branche min acc (_,_,br) = 
     acc || (
       let new_branche = 
-	Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in 
+	it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum br)) in 
       let free_rels_in_br = Termops.free_rels new_branche in 
       let max = min + scheme_info.Tactics.npredicates in 
       Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
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                                               *)