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

3 files changed, 12 insertions, 12 deletions

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