[api] Move structures deprecated in the API to the core.

We do up to `Term` which is the main bulk of the changes.

19 files changed, 54 insertions, 46 deletions

diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 09e645eea..d22024568 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -18,7 +18,7 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open Declarations
 open Mod_subst
 open Globnames
@@ -163,7 +163,7 @@ let label_of = function
 
 let fold_constr_with_full_binders g f n acc c =
   let open Context.Rel.Declaration in
-  match kind_of_term c with
+  match Constr.kind c with
   | Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _ -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
   | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
@@ -182,7 +182,7 @@ let fold_constr_with_full_binders g f n acc c =
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
-let rec traverse current ctx accu t = match kind_of_term t with
+let rec traverse current ctx accu t = match Constr.kind t with
 | Var id ->
   let body () = id |> Global.lookup_named |> NamedDecl.get_value in
   traverse_object accu body (VarRef id)
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 77eb968d4..afe932ead 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Globnames
 open Printer
 
@@ -28,4 +28,4 @@ val traverse :
    {!traverse} also applies. *)
 val assumptions :
   ?add_opaque:bool -> ?add_transparent:bool -> transparent_state ->
-     global_reference -> constr -> Term.types ContextObjectMap.t
+     global_reference -> constr -> types ContextObjectMap.t
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 539e5550f..3cf181441 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -13,6 +13,7 @@ open CErrors
 open Util
 open Pp
 open Term
+open Constr
 open Vars
 open Termops
 open Declarations
@@ -532,7 +533,7 @@ let eqI ind l =
     try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff 
     with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
       (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed.");
-  in (if Array.equal Term.eq_constr eA [||] then e else mkApp(e,eA)), eff
+  in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff
 
 (**********************************************************************)
 (* Boolean->Leibniz *)
diff --git a/vernac/class.ml b/vernac/class.ml
index 061f3efcc..f26599973 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -11,6 +11,7 @@ open Util
 open Pp
 open Names
 open Term
+open Constr
 open Vars
 open Termops
 open Entries
@@ -148,7 +149,7 @@ let get_target t ind =
       
 
 let prods_of t =
-  let rec aux acc d = match kind_of_term d with
+  let rec aux acc d = match Constr.kind d with
     | Prod (_,c1,c2) -> aux (c1::acc) c2
     | Cast (c,_,_) -> aux acc c
     | _ -> (d,acc)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 9a8fc9bc2..22117f7e1 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -9,6 +9,7 @@
 (*i*)
 open Names
 open Term
+open Constr
 open Vars
 open Environ
 open Nametab
diff --git a/vernac/classes.mli b/vernac/classes.mli
index fcdb5c3bc..c0f03227c 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -34,7 +34,7 @@ val declare_instance_constant :
   bool -> (* polymorphic *)
   Evd.evar_map -> (* Universes *)
   Constr.t -> (** body *)
-  Term.types -> (** type *)
+  Constr.types -> (** type *)
   Names.Id.t
 
 val new_instance :
diff --git a/vernac/command.ml b/vernac/command.ml
index f58ed065c..db3fa1955 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -10,6 +10,7 @@ open Pp
 open CErrors
 open Util
 open Term
+open Constr
 open Vars
 open Termops
 open Environ
@@ -44,7 +45,7 @@ let do_constraint poly l = Declare.do_constraint poly l
 
 let rec under_binders env sigma f n c =
   if Int.equal n 0 then f env sigma (EConstr.of_constr c) else
-    match kind_of_term c with
+    match Constr.kind c with
       | Lambda (x,t,c) ->
 	  mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c)
       | LetIn (x,b,t,c) ->
@@ -652,7 +653,7 @@ let extract_mutual_inductive_declaration_components indl =
 
 let is_recursive mie =
   let rec is_recursive_constructor lift typ =
-    match Term.kind_of_term typ with
+    match Constr.kind typ with
     | Prod (_,arg,rest) ->
         not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) ||
         is_recursive_constructor (lift+1) rest
diff --git a/vernac/command.mli b/vernac/command.mli
index 26b1d1aaf..5415d3308 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Entries
 open Libnames
 open Globnames
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 5dea0ba27..01a87818a 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -15,5 +15,5 @@ val declare_definition : Id.t -> definition_kind ->
   Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
-val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
+val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.UContext.t -> Id.t ->
   Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 4bdc93a36..c0ddc7e2c 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -21,6 +21,7 @@ open Names
 open Declarations
 open Entries
 open Term
+open Constr
 open Inductive
 open Decl_kinds
 open Indrec
@@ -458,7 +459,7 @@ let build_combined_scheme env schemes =
   let find_inductive ty =
     let (ctx, arity) = decompose_prod ty in
     let (_, last) = List.hd ctx in
-      match kind_of_term last with
+      match Constr.kind last with
 	| App (ind, args) ->
 	    let ind = destInd ind in
 	    let (_,spec) = Inductive.lookup_mind_specif env (fst ind) in
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index 659f12936..4b31389ab 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -8,7 +8,7 @@
 
 open Loc
 open Names
-open Term
+open Constr
 open Environ
 open Vernacexpr
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 22f0d199c..be9de5b30 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -14,6 +14,7 @@ open Util
 open Pp
 open Names
 open Term
+open Constr
 open Declarations
 open Declareops
 open Entries
@@ -62,7 +63,7 @@ let adjust_guardness_conditions const = function
      { const with const_entry_body =
         Future.chain const.const_entry_body
         (fun ((body, ctx), eff) ->
-          match kind_of_term body with
+          match Constr.kind body with
           | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
 (*      let possible_indexes =
 	List.map2 (fun i c -> match i with Some i -> i | None ->
@@ -97,7 +98,7 @@ let find_mutually_recursive_statements thms =
       let ind_hyps =
         List.flatten (List.map_i (fun i decl ->
           let t = RelDecl.get_type decl in
-          match kind_of_term t with
+          match Constr.kind t with
           | Ind ((kn,_ as ind),u) when
                 let mind = Global.lookup_mind kn in
                 mind.mind_finite <> Decl_kinds.CoFinite ->
@@ -107,7 +108,7 @@ let find_mutually_recursive_statements thms =
       let ind_ccl =
         let cclenv = push_rel_context hyps (Global.env()) in
         let whnf_ccl,_ = whd_all_stack cclenv Evd.empty (EConstr.of_constr ccl) in
-        match kind_of_term (EConstr.Unsafe.to_constr whnf_ccl) with
+        match Constr.kind (EConstr.Unsafe.to_constr whnf_ccl) with
         | Ind ((kn,_ as ind),u) when
               let mind = Global.lookup_mind kn in
               Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
@@ -246,7 +247,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
   | Some body ->
       let body = norm body in
       let k = Kindops.logical_kind_of_goal_kind kind in
-      let rec body_i t = match kind_of_term t with
+      let rec body_i t = match Constr.kind t with
         | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
         | CoFix (0,decls) -> mkCoFix (i,decls)
         | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 1e23c7314..1f46a385d 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Decl_kinds
 
 type 'a declaration_hook
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 785c842ba..e23146273 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -13,6 +13,7 @@ open Declare
 *)
 
 open Term
+open Constr
 open Vars
 open Names
 open Evd
@@ -55,7 +56,7 @@ let subst_evar_constr evs n idf t =
   let seen = ref Int.Set.empty in
   let transparent = ref Id.Set.empty in
   let evar_info id = List.assoc_f Evar.equal id evs in
-  let rec substrec (depth, fixrels) c = match kind_of_term c with
+  let rec substrec (depth, fixrels) c = match Constr.kind c with
     | Evar (k, args) ->
 	let { ev_name = (id, idstr) ;
 	      ev_hyps = hyps ; ev_chop = chop } =
@@ -85,15 +86,15 @@ let subst_evar_constr evs n idf t =
 	  in aux hyps args []
 	in
 	  if List.exists
-            (fun x -> match kind_of_term x with
+            (fun x -> match Constr.kind x with
             | Rel n -> Int.List.mem n fixrels
             | _ -> false) args
           then
 	    transparent := Id.Set.add idstr !transparent;
 	  mkApp (idf idstr, Array.of_list args)
     | Fix _ ->
-	map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
-    | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
+	Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c
+    | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c
   in
   let t' = substrec (0, []) t in
     t', !seen, !transparent
@@ -103,9 +104,9 @@ let subst_evar_constr evs n idf t =
   where n binders were passed through. *)
 let subst_vars acc n t =
   let var_index id = Util.List.index Id.equal id acc in
-  let rec substrec depth c = match kind_of_term c with
+  let rec substrec depth c = match Constr.kind c with
     | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
-    | _ -> map_constr_with_binders succ substrec depth c
+    | _ -> Constr.map_with_binders succ substrec depth c
   in
     substrec 0 t
 
@@ -144,7 +145,7 @@ let rec chop_product n t =
   let pop t = Vars.lift (-1) t in
   if Int.equal n 0 then Some t
   else
-    match kind_of_term t with
+    match Constr.kind t with
       | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (pop b) else None
       | _ -> None
 
@@ -273,7 +274,7 @@ let explain_no_obligations = function
   | None -> str "No obligations remaining"
 
 type obligation_info =
-    (Names.Id.t * Term.types * Evar_kinds.t Loc.located *
+    (Names.Id.t * types * Evar_kinds.t Loc.located *
        (bool * Evar_kinds.obligation_definition_status)
        * Int.Set.t * unit Proofview.tactic option) array
 
@@ -384,7 +385,7 @@ let subst_deps expand obls deps t =
     (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
 
 let rec prod_app t n =
-  match kind_of_term (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with
+  match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with
     | Prod (_,_,b) -> subst1 n b
     | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
     | _ ->
@@ -400,13 +401,13 @@ let replace_appvars subst =
     let f, l = decompose_app c in
       if isVar f then
 	try
-	  let c' = List.map (map_constr aux) l in
+	  let c' = List.map (Constr.map aux) l in
 	  let (t, b) = Id.List.assoc (destVar f) subst in
 	    mkApp (delayed_force hide_obligation, 
 		   [| prod_applist t c'; applistc b c' |])
-	with Not_found -> map_constr aux c
-      else map_constr aux c
-  in map_constr aux
+	with Not_found -> Constr.map aux c
+      else Constr.map aux c
+  in Constr.map aux
        
 let subst_prog expand obls ints prg =
   let subst = obl_substitution expand obls ints in
@@ -490,7 +491,7 @@ let declare_definition prg =
   cst
 
 let rec lam_index n t acc =
-  match kind_of_term t with
+  match Constr.kind t with
     | Lambda (Name n', _, _) when Id.equal n n' ->
       acc
     | Lambda (_, _, b) ->
@@ -566,9 +567,9 @@ let declare_mutual_definition l =
 let decompose_lam_prod c ty =
   let open Context.Rel.Declaration in
   let rec aux ctx c ty =
-    match kind_of_term c, kind_of_term ty with
+    match Constr.kind c, Constr.kind ty with
     | LetIn (x, b, t, c), LetIn (x', b', t', ty)
-	 when eq_constr b b' && eq_constr t t' ->
+	 when Constr.equal b b' && Constr.equal t t' ->
        let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in
        aux ctx' c ty
     | _, LetIn (x', b', t', ty) ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 11c2553ae..d037fdcd8 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Environ
-open Term
+open Constr
 open Evd
 open Names
 open Globnames
@@ -39,7 +39,7 @@ val eterm_obligations : env -> Id.t -> evar_map -> int ->
        translation from obligation identifiers to constrs, new term, new type *)
 
 type obligation_info =
-  (Id.t * Term.types * Evar_kinds.t Loc.located *
+  (Id.t * types * Evar_kinds.t Loc.located *
       (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array
     (* ident, type, location, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)
@@ -51,13 +51,13 @@ type progress = (* Resolution status of a program *)
 
 val default_tactic : unit Proofview.tactic ref
 
-val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> 
+val add_definition : Names.Id.t -> ?term:constr -> types -> 
   Evd.evar_universe_context ->
   ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
   ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
-  ?reduce:(Term.constr -> Term.constr) ->
+  ?reduce:(constr -> constr) ->
   ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
 
 type notations =
@@ -68,13 +68,13 @@ type fixpoint_kind =
   | IsCoFixpoint
 
 val add_mutual_definitions :
-  (Names.Id.t * Term.constr * Term.types *
+  (Names.Id.t * constr * types *
       (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
   Evd.evar_universe_context ->
   ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
-  ?reduce:(Term.constr -> Term.constr) ->
+  ?reduce:(constr -> constr) ->
   ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
   notations ->
   fixpoint_kind -> unit
diff --git a/vernac/record.ml b/vernac/record.ml
index 5533fe5b3..1fd43624a 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -13,6 +13,7 @@ open Names
 open Globnames
 open Nameops
 open Term
+open Constr
 open Vars
 open Environ
 open Declarations
@@ -229,7 +230,7 @@ exception NotDefinable of record_error
 let subst_projection fid l c =
   let lv = List.length l in
   let bad_projs = ref [] in
-  let rec substrec depth c = match kind_of_term c with
+  let rec substrec depth c = match Constr.kind c with
     | Rel k ->
 	(* We are in context [[params;fields;x:ind;...depth...]] *)
         if k <= depth+1 then
@@ -244,7 +245,7 @@ let subst_projection fid l c =
                   " field which has no name.")
         else
 	  mkRel (k-lv)
-    | _ -> map_constr_with_binders succ substrec depth c
+    | _ -> Constr.map_with_binders succ substrec depth c
   in
   let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *)
   let c'' = substrec 0 c' in
diff --git a/vernac/record.mli b/vernac/record.mli
index 1bcbf39b7..33c2fba89 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Vernacexpr
 open Constrexpr
 open Impargs
diff --git a/vernac/search.ml b/vernac/search.ml
index 0f56f81e7..6da6a0c2d 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -9,7 +9,7 @@
 open Pp
 open Util
 open Names
-open Term
+open Constr
 open Declarations
 open Libobject
 open Environ
diff --git a/vernac/search.mli b/vernac/search.mli
index db54d732b..2eda3980a 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open Pattern
 open Globnames