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

7 files changed, 28 insertions, 28 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index ec3a8d6c9d..36e8add7e9 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1081,7 +1081,7 @@ let compileAutoArg contac = function
 	 tclFIRST 
            (List.map 
               (fun (id,_,typ) -> 
-                let cl = snd (decompose_prod typ) in
+                let cl = (strip_prod_assum typ) in
                  if Hipattern.is_conjunction cl
 		 then 
 		   tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac] 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index b556676ee6..b6272115a8 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -888,7 +888,7 @@ let unfold_all t =
     | _ -> assert false
 
 let decomp_prod env evm n c = 
-  snd (Reductionops.decomp_n_prod env evm n c)
+  snd (Reductionops.splay_prod_n env evm n c)
 
 let rec decomp_pointwise n c =
   if n = 0 then c
@@ -1402,7 +1402,7 @@ open Entries
 open Libnames
 
 let respect_projection r ty =
-  let ctx, inst = Sign.decompose_prod_assum ty in
+  let ctx, inst = decompose_prod_assum ty in
   let mor, args = destApp inst in
   let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
   let app = mkApp (Lazy.force respect_proj, 
@@ -1414,7 +1414,7 @@ let declare_projection n instance_id r =
   let c = constr_of_global r in
   let term = respect_projection c ty in
   let typ = Typing.type_of (Global.env ()) Evd.empty term in
-  let ctx, typ = Sign.decompose_prod_assum typ in
+  let ctx, typ = decompose_prod_assum typ in
   let typ =
     let n = 
       let rec aux t = 
@@ -1430,7 +1430,7 @@ let declare_projection n instance_id r =
 	  | _ -> typ
       in aux init
     in
-    let ctx,ccl = Reductionops.decomp_n_prod (Global.env()) Evd.empty (3 * n) typ
+    let ctx,ccl = Reductionops.splay_prod_n (Global.env()) Evd.empty (3 * n) typ
     in it_mkProd_or_LetIn ccl ctx 
   in
   let typ = it_mkProd_or_LetIn typ ctx in
@@ -1799,7 +1799,7 @@ let setoid_transitivity c gl =
 *)
 let setoid_symmetry_in id gl =
   let ctype = pf_type_of gl (mkVar id) in
-  let binders,concl = Sign.decompose_prod_assum ctype in
+  let binders,concl = decompose_prod_assum ctype in
   let (equiv, args) = decompose_app concl in
   let rec split_last_two = function
     | [c1;c2] -> [],(c1, c2)
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 741874cb31..7e25b072ea 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -1265,7 +1265,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let gen_arities = Inductive.arities_of_constructors ind spec in
 	let f_ids typ = 
 	  let sign = 
-	    fst (Sign.decompose_prod_assum (Term.prod_applist typ params)) in
+	    (prod_assum (Term.prod_applist typ params)) in
 	    find_intro_names sign gls in
 	let constr_args_ids = Array.map f_ids gen_arities in
 	let case_term =	 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 9fb4becda2..5f7405c93b 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -94,7 +94,7 @@ let match_with_one_constructor style t =
       then
 	if style = Some true (* strict conjunction *) then
 	  let ctx = 
-	    fst (decompose_prod_assum (snd 
+	    (prod_assum (snd 
 	      (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in
 	  if 
 	    List.for_all
@@ -104,7 +104,7 @@ let match_with_one_constructor style t =
 	  else None
 	else
 	  let ctyp = prod_applist mip.mind_nf_lc.(0) args in
-	  let cargs = List.map pi3 (fst (decompose_prod_assum ctyp)) in
+	  let cargs = List.map pi3 ((prod_assum ctyp)) in
 	  if style <> Some false || has_nodep_prod ctyp then
 	    (* Record or non strict conjunction *)
 	    Some (hdapp,List.rev cargs)
@@ -134,7 +134,7 @@ let is_record t =
 
 let test_strict_disjunction n lc =
   array_for_all_i (fun i c ->
-    match fst (decompose_prod_assum (snd (decompose_prod_n_assum n c))) with
+    match (prod_assum (snd (decompose_prod_n_assum n c))) with
     | [_,None,c] -> c = mkRel (n - i)
     | _ -> false) 0 lc
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b6923bb83f..46ce6e20b5 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -127,7 +127,7 @@ let make_inv_predicate env sigma indf realargs id status concl =
      push <Ai>(mkRel k)=ai (when   Ai is closed).
    In any case, we carry along the rest of pairs *)
   let rec build_concl eqns n = function
-    | [] -> (prod_it concl eqns,n)
+    | [] -> (it_mkProd concl eqns,n)
     | (ai,(xi,ti))::restlist ->
         let (lhs,eqnty,rhs) =
           if closed0 ti then 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index f74d6dfdfb..fcb1d2bb53 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -967,7 +967,7 @@ let check_a env a =
 
 let check_eq env a_quantifiers_rev a aeq =
  let typ =
-  Sign.it_mkProd_or_LetIn
+  it_mkProd_or_LetIn
    (mkApp ((Lazy.force coq_relation),[| apply_to_rels a a_quantifiers_rev |]))
    a_quantifiers_rev in
  if
@@ -981,7 +981,7 @@ let check_property env a_quantifiers_rev a aeq strprop coq_prop t =
  if
   not
    (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
-    (Sign.it_mkProd_or_LetIn
+    (it_mkProd_or_LetIn
      (mkApp ((Lazy.force coq_prop),
        [| apply_to_rels a   a_quantifiers_rev ;
           apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev))
@@ -1002,7 +1002,7 @@ let check_setoid_theory env a_quantifiers_rev a aeq th =
  if
   not
    (is_conv env Evd.empty (Typing.type_of env Evd.empty th)
-    (Sign.it_mkProd_or_LetIn
+    (it_mkProd_or_LetIn
      (mkApp ((Lazy.force coq_Setoid_Theory),
        [| apply_to_rels a   a_quantifiers_rev ;
           apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev))
@@ -1039,7 +1039,7 @@ let int_add_relation id a aeq refl sym trans =
    Declare.declare_internal_constant id
     (DefinitionEntry
       {const_entry_body =
-        Sign.it_mkLambda_or_LetIn x_relation_class
+        it_mkLambda_or_LetIn x_relation_class
          ([ Name (id_of_string "v"),None,mkRel 1;
             Name (id_of_string "X"),None,mkType (Termops.new_univ ())] @
             a_quantifiers_rev);
@@ -1059,7 +1059,7 @@ let int_add_relation id a aeq refl sym trans =
    Declare.declare_internal_constant id_precise
     (DefinitionEntry
       {const_entry_body =
-        Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev;
+        it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev;
        const_entry_type = None;
        const_entry_opaque = false;
        const_entry_boxed = Flags.boxed_definitions() },
@@ -1119,7 +1119,7 @@ let int_add_relation id a aeq refl sym trans =
       let _ =
        Declare.declare_internal_constant mor_name
         (DefinitionEntry
-          {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev;
+          {const_entry_body = it_mkLambda_or_LetIn lemma a_quantifiers_rev;
            const_entry_type = None;
            const_entry_opaque = false;
           const_entry_boxed = Flags.boxed_definitions()},
@@ -1153,15 +1153,15 @@ let add_setoid id a aeq th =
    let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
    let th_instance = apply_to_rels th a_quantifiers_rev in
    let refl =
-    Sign.it_mkLambda_or_LetIn
+    it_mkLambda_or_LetIn
      (mkApp ((Lazy.force coq_seq_refl),
        [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in
    let sym =
-    Sign.it_mkLambda_or_LetIn
+    it_mkLambda_or_LetIn
      (mkApp ((Lazy.force coq_seq_sym),
        [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in
    let trans =
-    Sign.it_mkLambda_or_LetIn
+    it_mkLambda_or_LetIn
      (mkApp ((Lazy.force coq_seq_trans),
        [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in
    int_add_relation id a aeq (Some refl) (Some sym) (Some trans)
@@ -1976,7 +1976,7 @@ let setoid_replace_in  tac_opt id relation c1 c2 ~new_goals gl =
 
 (* let setoid_symmetry_in id gl = *)
 (*   let ctype = pf_type_of gl (mkVar id) in *)
-(*   let binders,concl = Sign.decompose_prod_assum ctype in *)
+(*   let binders,concl = decompose_prod_assum ctype in *)
 (*   let (equiv, args) = decompose_app concl in *)
 (*   let rec split_last_two = function *)
 (*     | [c1;c2] -> [],(c1, c2) *)
@@ -2009,7 +2009,7 @@ let setoid_replace_in  tac_opt id relation c1 c2 ~new_goals gl =
 (*         | Some trans -> *)
 (*            let transty = nf_betaiota (pf_type_of gl trans) in *)
 (*            let argsrev, _ = *)
-(*             Reductionops.decomp_n_prod (pf_env gl) Evd.empty 2 transty in *)
+(*             Reductionops.splay_prod_n (pf_env gl) Evd.empty 2 transty in *)
 (*            let binder = *)
 (*             match List.rev argsrev with *)
 (*                _::(Name n2,None,_)::_ -> Rawterm.NamedHyp n2 *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 44f07d37b5..c8d078aee2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -709,7 +709,7 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 let descend_in_conjunctions with_evars tac exit c gl =
   try
     let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-    match match_with_conjunction (snd (decompose_prod t)) with
+    match match_with_conjunction ((strip_prod t)) with
     | Some _ ->
 	let n = (mis_constr_nargs mind).(0) in
 	let sort = elimination_sort_of_goal gl in
@@ -1236,7 +1236,7 @@ let ipat_of_name = function
 
 let allow_replace c gl = function (* A rather arbitrary condition... *)
   | Some (_, IntroIdentifier id) ->
-      fst (decompose_app (snd (decompose_lam_assum c))) = mkVar id
+      fst (decompose_app ((strip_lam_assum c))) = mkVar id
   | _ ->
       false
 
@@ -2086,7 +2086,7 @@ let abstract_args gl id =
 	*)
 	let aux (prod, ctx, ctxenv, c, args, eqs, refls, vars, env) arg =
 	  let (name, _, ty), arity = 
-	    let rel, c = Reductionops.decomp_n_prod env sigma 1 prod in
+	    let rel, c = Reductionops.splay_prod_n env sigma 1 prod in
 	      List.hd rel, c
 	  in
 	  let argty = pf_type_of gl arg in
@@ -2224,7 +2224,7 @@ let decompose_paramspred_branch_args elimt =
   let rec cut_noccur elimt acc2 : rel_context * rel_context * types =
     match kind_of_term elimt with
       | Prod(nme,tpe,elimt') -> 
-	  let hd_tpe,_ = decompose_app (snd (decompose_prod_assum tpe)) in
+	  let hd_tpe,_ = decompose_app ((strip_prod_assum tpe)) in
 	  if not (occur_rel 1 elimt') && isRel hd_tpe	    
 	  then cut_noccur elimt' ((nme,None,tpe)::acc2)
 	  else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl
@@ -2455,7 +2455,7 @@ let find_elim_signature isrec elim hyp0 gl =
 	let elimt = pf_type_of gl elimc in
 	((elimc, NoBindings), elimt), mkInd mind
     | Some (elimc,lbind as e) ->
-	let ind_type_guess,_ = decompose_app (snd (decompose_prod tmptyp0)) in
+	let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in
 	(e, pf_type_of gl elimc), ind_type_guess in
   let indsign,elim_scheme =
     compute_elim_signature elimc elimt hyp0 ind in
@@ -2599,7 +2599,7 @@ let induction_from_context isrec with_evars elim_info (hyp0,lbind) names
   let tmptyp0 =	pf_get_hyp_typ gl hyp0 in
   let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
   let indvars =
-    find_atomic_param_of_ind scheme.nparams (snd (decompose_prod typ0)) in
+    find_atomic_param_of_ind scheme.nparams ((strip_prod typ0)) in
   let induct_tac = tclTHENLIST [
     induction_tac with_evars (hyp0,lbind) typ0 scheme;
     tclTRY (unfold_body hyp0);