4 files changed, 5 insertions, 5 deletions
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