15 files changed, 23 insertions, 27 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index faabd7c14..ccef9ab96 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -12,13 +12,13 @@
 
 open CErrors
 open Pp
-open Goptions
 open Names
-open Term
+open Sorts
 open Constr
 open Vars
-open Tacmach
 open Evd
+open Goptions
+open Tacmach
 open Util
 
 let init_size=5
@@ -437,7 +437,7 @@ and make_app l=function
 and applist_proj c l =
   match c with
   | Symb s -> applist_projection s l
-  | _ -> applistc (constr_of_term c) l
+  | _ -> Term.applistc (constr_of_term c) l
 and applist_projection c l =
   match Constr.kind c with
   | Const c when Environ.is_projection (fst c) (Global.env()) ->
@@ -447,10 +447,10 @@ and applist_projection c l =
       let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *)
       let pb = Environ.lookup_projection p (Global.env()) in
       let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
-	it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
+      Term.it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
     | hd :: tl ->
-      applistc (mkProj (p, hd)) tl)
-  | _ -> applistc c l
+      Term.applistc (mkProj (p, hd)) tl)
+  | _ -> Term.applistc c l
 
 let rec canonize_name sigma c =
   let c = EConstr.Unsafe.to_constr c in
@@ -838,7 +838,7 @@ let complete_one_class state i=
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
 	    pac.args in
-	let typ = prod_applist _c (List.rev _args) in
+        let typ = Term.prod_applist _c (List.rev _args) in
 	let ct = app (term state.uf i) typ pac.arity in
 	  state.uf.epsilons <- pac :: state.uf.epsilons;
 	  ignore (add_term state ct)
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7dec34d4d..8642df684 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -12,7 +12,6 @@ open Evd
 open Names
 open Inductiveops
 open Declarations
-open Term
 open Constr
 open EConstr
 open Vars
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 995d5fd19..5903733a6 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -486,7 +486,7 @@ let check_loaded_modfile mp = match base_mp mp with
       if not (Library.library_is_loaded dp) then begin
 	match base_mp (Lib.current_mp ()) with
 	  | MPfile dp' when not (DirPath.equal dp dp') ->
-	      err (str "Please load library " ++ pr_dirpath dp ++ str " first.")
+            err (str "Please load library " ++ DirPath.print dp ++ str " first.")
 	  | _ -> ()
       end
   | _ -> ()
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index f660ba734..d46201335 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -11,7 +11,7 @@ open Formula
 open Sequent
 open Rules
 open Instances
-open Term
+open Constr
 open Tacmach.New
 open Tacticals.New
 
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index d6309b057..1a6eba8c6 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -235,8 +235,8 @@ let constant str = Universes.constr_of_global
   @@ Coqlib.coq_reference "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
-  [AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not")));
-   AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))]
+  [AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "not")));
+   AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "iff")))]
 
 let normalize_evaluables=
   Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 29e824f44..62ca70626 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,7 +1,7 @@
 open Printer
 open CErrors
 open Util
-open Term
+open Constr
 open EConstr
 open Vars
 open Namegen
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 3899bc709..996e2b6af 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,7 +1,8 @@
 open Printer
 open CErrors
-open Util
 open Term
+open Sorts
+open Util
 open Constr
 open Vars
 open Namegen
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index d04b7a33d..fa4353630 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1,7 +1,6 @@
 open Printer
 open Pp
 open Names
-open Term
 open Constr
 open Vars
 open Glob_term
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f01b6669d..9e22ad306 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,7 +1,8 @@
 open CErrors
+open Sorts
 open Util
 open Names
-open Term
+open Constr
 open EConstr
 open Pp
 open Indfun_common
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 04d729b10..3089ec470 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -9,7 +9,6 @@
 
 module CVars = Vars
 
-open Term
 open Constr
 open EConstr
 open Vars
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 578ebd6f7..d6cfa3cf9 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -315,7 +315,8 @@ let project_hint pri l2r r =
   in
   let ctx = Evd.universe_context_set sigma in
   let c = EConstr.to_constr sigma c in
-  let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
+  let poly = Flags.use_polymorphic_flag () in
+  let c = Declare.declare_definition ~poly ~internal:Declare.InternalTacticRequest id (c,ctx) in
   let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
     (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 96bf31b11..0ea8904f2 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -104,7 +104,7 @@
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open EConstr
 open Pattern
 open Patternops
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 5397b0065..32a1c07b2 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -7,7 +7,6 @@
  *************************************************************************)
 
 open Names
-open Term
 open Constr
 
 let module_refl_name = "ReflOmegaCore"
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 274c7110c..bd9633afb 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -342,7 +342,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
     let sort = elimination_sort_of_goal gl in
     let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
     if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
-    let elim, _ = Term.destConst elim in          
+    let elim, _ = destConst elim in
     let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in
     let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r")  in 
     let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index a707226cd..5c1b399a8 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -8,11 +8,12 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
+open Pp
 open Names
+open Constr
 open Tacmach
 
 open Ssrmatching_plugin.Ssrmatching
-
 open Ssrprinters
 open Ssrcommon
 open Ssrtacticals
@@ -30,10 +31,6 @@ let ssrposetac ist (id, (_, t)) gl =
   let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in
   posetac id t (pf_merge_uc ucst gl)
 
-open Pp
-open Term
-open Constr
-
 let ssrsettac ist id ((_, (pat, pty)), (_, occ)) gl =
   let pat = interp_cpattern ist gl pat (Option.map snd pty) in
   let cl, sigma, env = pf_concl gl, project gl, pf_env gl in