Remove some occurrences of "open Termops"

Functions from Termops were sometimes fully qualified, sometimes not
in the same module. This commit makes their usage more uniform.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13470 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 26 insertions, 28 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 941b6f7df5..acded3ac58 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -16,7 +16,6 @@ open Names
 open Libnames
 open Nameops
 open Term
-open Termops
 open Namegen
 open Declarations
 open Entries
@@ -55,7 +54,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
   if not (List.mem kind (elim_sorts specif)) then
     raise
       (RecursionSchemeError
-	 (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind)));
+	 (NotAllowedCaseAnalysis (false, Termops.new_sort_in_family kind, ind)));
 
   let ndepar = mip.mind_nrealargs_ctxt + 1 in
 
@@ -63,7 +62,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
   (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
   let env' = push_rel_context lnamespar env in
 
-  let indf = make_ind_family(ind, extended_rel_list 0 lnamespar) in
+  let indf = make_ind_family(ind, Termops.extended_rel_list 0 lnamespar) in
   let constrs = get_constructors env indf in
 
   let rec add_branch env k =
@@ -79,8 +78,8 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
       let pbody =
         appvect
           (mkRel (ndepar + nbprod),
-           if dep then extended_rel_vect 0 deparsign
-           else extended_rel_vect 1 arsign) in
+           if dep then Termops.extended_rel_vect 0 deparsign
+           else Termops.extended_rel_vect 1 arsign) in
       let p =
 	it_mkLambda_or_LetIn_name env'
 	  ((if dep then mkLambda_name env' else mkLambda)
@@ -90,7 +89,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
       it_mkLambda_or_LetIn_name env'
        	(mkCase (ci, lift ndepar p,
 		     mkRel 1,
-		     rel_vect ndepar k))
+		     Termops.rel_vect ndepar k))
        	deparsign
     else
       let cs = lift_constructor (k+1) constrs.(k) in
@@ -98,7 +97,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
       mkLambda_string "f" t
 	(add_branch (push_rel (Anonymous, None, t) env) (k+1))
   in
-  let typP = make_arity env' dep indf (new_sort_in_family kind) in
+  let typP = make_arity env' dep indf (Termops.new_sort_in_family kind) in
   it_mkLambda_or_LetIn_name env
     (mkLambda_string "P" typP
        (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
@@ -138,7 +137,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	    let base = applist (lift i pk,realargs) in
             if depK then
 	      Reduction.beta_appvect
-                base [|applist (mkRel (i+1),extended_rel_list 0 sign)|]
+                base [|applist (mkRel (i+1), Termops.extended_rel_list 0 sign)|]
             else
 	      base
       	| _ -> assert false
@@ -210,7 +209,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
      	| Ind _ ->
             let realargs = list_skipn nparrec largs
-            and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in
+            and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in
             applist(lift i fk,realargs@[arg])
      	| _ -> assert false
     in
@@ -296,7 +295,7 @@ let mis_make_indrec env sigma listdepkind mib =
 
             (* arity in the context of the fixpoint, i.e.
                P1..P_nrec f1..f_nbconstruct *)
-	    let args = extended_rel_list (nrec+nbconstruct) lnamesparrec in
+	    let args = Termops.extended_rel_list (nrec+nbconstruct) lnamesparrec in
 	    let indf = make_ind_family(indi,args) in
 
 	    let arsign,_ = get_arity env indf in
@@ -310,15 +309,15 @@ let mis_make_indrec env sigma listdepkind mib =
 
             (* constructors in context of the Cases expr, i.e.
                P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
-	    let args' = extended_rel_list (dect+nrec) lnamesparrec in
-	    let args'' = extended_rel_list ndepar lnonparrec in
+	    let args' = Termops.extended_rel_list (dect+nrec) lnamesparrec in
+	    let args'' = Termops.extended_rel_list ndepar lnonparrec in
             let indf' = make_ind_family(indi,args'@args'') in
 
 	    let branches =
 	      let constrs = get_constructors env indf' in
-	      let fi = rel_vect (dect-i-nctyi) nctyi in
+	      let fi = Termops.rel_vect (dect-i-nctyi) nctyi in
 	      let vecfi = Array.map
-		(fun f -> appvect (f,extended_rel_vect ndepar lnonparrec))
+		(fun f -> appvect (f, Termops.extended_rel_vect ndepar lnonparrec))
 		fi
 	      in
 		array_map3
@@ -339,9 +338,9 @@ let mis_make_indrec env sigma listdepkind mib =
 	    let deparsign' = (Anonymous,None,depind')::arsign' in
 
 	    let pargs =
-	      let nrpar = extended_rel_list (2*ndepar) lnonparrec
-	      and nrar = if dep then extended_rel_list 0 deparsign'
-		else extended_rel_list 1 arsign'
+	      let nrpar = Termops.extended_rel_list (2*ndepar) lnonparrec
+	      and nrar = if dep then Termops.extended_rel_list 0 deparsign'
+		else Termops.extended_rel_list 1 arsign'
 	      in nrpar@nrar
 
 	    in
@@ -360,15 +359,15 @@ let mis_make_indrec env sigma listdepkind mib =
 		  (mkCase (ci, pred,
 		          mkRel 1,
 			  branches))
-		  (lift_rel_context nrec deparsign)
+		  (Termops.lift_rel_context nrec deparsign)
 	    in
 
 	    (* type of i-th component of the mutual fixpoint *)
 
 	    let typtyi =
 	      let concl =
-		let pargs = if dep then extended_rel_vect 0 deparsign
-		  else extended_rel_vect 1 arsign
+		let pargs = if dep then Termops.extended_rel_vect 0 deparsign
+		  else Termops.extended_rel_vect 1 arsign
 		in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
 	      in it_mkProd_or_LetIn_name env
 		concl
@@ -395,7 +394,7 @@ let mis_make_indrec env sigma listdepkind mib =
 	    else
 	      let recarg = (dest_subterms recargsvec.(tyi)).(j) in
 	      let recarg = recargpar@recarg in
-	      let vargs = extended_rel_list (nrec+i+j) lnamesparrec in
+	      let vargs = Termops.extended_rel_list (nrec+i+j) lnamesparrec in
 	      let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in
 	      let p_0 =
 		type_rec_branch
@@ -409,8 +408,8 @@ let mis_make_indrec env sigma listdepkind mib =
     in
     let rec put_arity env i = function
       | (indi,_,_,dep,kinds)::rest ->
-	  let indf = make_ind_family (indi,extended_rel_list i lnamesparrec) in
-	  let typP = make_arity env dep indf (new_sort_in_family kinds) in
+	  let indf = make_ind_family (indi, Termops.extended_rel_list i lnamesparrec) in
+	  let typP = make_arity env dep indf (Termops.new_sort_in_family kinds) in
 	    mkLambda_string "P" typP
 	      (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
       | [] ->
@@ -504,7 +503,7 @@ let check_arities listdepkind =
        let kelim = elim_sorts (mibi,mipi) in
        if not (List.exists ((=) kind) kelim) then raise
 	 (RecursionSchemeError
-	   (NotAllowedCaseAnalysis (true,new_sort_in_family kind,mind)))
+	   (NotAllowedCaseAnalysis (true, Termops.new_sort_in_family kind,mind)))
        else if List.mem ni ln then raise
 	 (RecursionSchemeError (NotMutualInScheme (mind,mind)))
        else ni::ln)
@@ -569,5 +568,5 @@ let lookup_eliminator ind_sp s =
       (strbrk "Cannot find the elimination combinator " ++
        pr_id id ++ strbrk ", the elimination of the inductive definition " ++
        pr_global_env Idset.empty (IndRef ind_sp) ++
-       strbrk " on sort " ++ pr_sort_family s ++
+       strbrk " on sort " ++ Termops.pr_sort_family s ++
        strbrk " is probably not allowed.")
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index d477ec34ac..ccedf1520d 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -19,7 +19,6 @@ open Names
 open Libnames
 open Nametab
 open Term
-open Termops
 open Typeops
 open Libobject
 open Library
@@ -206,7 +205,7 @@ let cs_pattern_of_constr t =
 	      _ -> raise Not_found
 	end
     | Rel n -> Default_cs, pred n, []
-    | Prod (_,a,b) when not (dependent (mkRel 1) b) -> Prod_cs, -1, [a;pop b]
+    | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b]
     | Sort s -> Sort_cs (family_of_sort s), -1, []
     | _ ->
 	begin
@@ -240,7 +239,7 @@ let compute_canonical_projections (con,ind) =
                      (let con_pp = Nametab.pr_global_env Idset.empty (ConstRef con)
                       and proji_sp_pp = Nametab.pr_global_env Idset.empty (ConstRef proji_sp) in
 		      msg_warning (str "No global reference exists for projection value"
-                                   ++ print_constr t ++ str " in instance "  
+                                   ++ Termops.print_constr t ++ str " in instance "  
                                    ++ con_pp ++ str " of " ++ proji_sp_pp ++ str ", ignoring it."));
 		   l
 	       end