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

1 files changed, 11 insertions, 11 deletions

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 *)