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

6 files changed, 7 insertions, 7 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index f577355d37..d2d399f100 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -199,7 +199,7 @@ let build_id_coercion idf_opt source =
   let c = match constant_opt_value env (destConst vs) with
     | Some c -> c
     | None -> error_not_transparent source in
-  let lams,t = Sign.decompose_lam_assum c in
+  let lams,t = decompose_lam_assum c in
   let val_f =
     it_mkLambda_or_LetIn
       (mkLambda (Name (id_of_string "x"),
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 47c51b83fd..07f5019565 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -355,7 +355,7 @@ let adjust_guardness_conditions const =
   | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
       let possible_indexes =
 	List.map (fun c ->
-	  interval 0 (List.length (fst (Sign.decompose_lam_assum c))))
+	  interval 0 (List.length ((lam_assum c))))
 	  (Array.to_list fixdefs) in
       let indexes = search_guard dummy_loc (Global.env()) possible_indexes fixdecls in 
       { const with const_entry_body = mkFix ((indexes,0),fixdecls) }
@@ -1125,7 +1125,7 @@ let look_for_mutual_statements thms =
     (* common coinductive conclusion *)
     let n = List.length thms in
     let inds = List.map (fun (id,(t,_) as x) -> 
-      let (hyps,ccl) = Sign.decompose_prod_assum t in
+      let (hyps,ccl) = decompose_prod_assum t in
       let whnf_hyp_hds = map_rel_context_with_binders
         (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c)))
         hyps in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 1bc4e4f33c..52581a15df 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -92,7 +92,7 @@ let explain_elim_arity env ind sorts c pj okinds =
 	| WrongArity ->
 	  "wrong arity" in
       let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in
-      let ppt = pr_lconstr_env env (snd (decompose_prod_assum pj.uj_type)) in
+      let ppt = pr_lconstr_env env ((strip_prod_assum pj.uj_type)) in
       hov 0
 	(str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
 	 str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 79d34e878e..9978d7bf6d 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -269,7 +269,7 @@ let set_rigid c =
 
 let declare_instance_cst glob con =
   let instance = Typeops.type_of_constant (Global.env ()) con in
-  let _, r = Sign.decompose_prod_assum instance in
+  let _, r = decompose_prod_assum instance in
     match class_of_constr r with
       | Some tc -> add_instance (new_instance tc None glob con)
       | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
diff --git a/toplevel/record.mli b/toplevel/record.mli
index b74c1a4af7..3fe18e1926 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -29,7 +29,7 @@ val declare_projections :
 
 val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> 
   manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *)
-  Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *)
+  Impargs.manual_explicitation list list -> rel_context -> (* fields *)
   ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
   bool -> (* coercion? *)
   bool list -> (* field coercions *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 465c55a4b4..a4d3e5458a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -119,7 +119,7 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
 let show_intro all =
   let pf = get_pftreestate() in
   let gl = nth_goal_of_pftreestate 1 pf in
-  let l,_= Sign.decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
+  let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
   if all 
   then 
     let lid = Tactics.find_intro_names l gl in