Merge PR #6969: [api] Remove functions deprecated in 8.8

8 files changed, 8 insertions, 97 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 4ee13c961..3eb5acfc5 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -600,8 +600,3 @@ let _ = Goptions.declare_bool_option {
   Goptions.optread = (fun () -> !asymmetric_patterns);
   Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
 }
-
-(************************************************************************)
-(* Deprecated *)
-let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c
-let prod_constr_expr c bl =  mkCProdN ?loc:(local_binders_loc bl) bl c
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index d038bd71a..2df9e5a8c 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -60,14 +60,6 @@ val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr
 val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr
 (** Apply a list of pattern arguments to a pattern *)
 
-(** @deprecated variant of mkCLambdaN *)
-val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
-[@@ocaml.deprecated "deprecated variant of mkCLambdaN"]
-
-(** @deprecated variant of mkCProdN *)
-val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
-[@@ocaml.deprecated "deprecated variant of mkCProdN"]
-
 (** {6 Destructors}*)
 
 val coerce_reference_to_id : reference -> Id.t
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7792eff66..86f6ce9ae 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -28,7 +28,6 @@ open Pattern
 open Nametab
 open Notation
 open Detyping
-open Misctypes
 open Decl_kinds
 
 module NamedDecl = Context.Named.Declaration
@@ -931,7 +930,7 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 and factorize_prod scopes vars na bk aty c =
   let store, get = set_temporary_memory () in
   match na, DAst.get c with
-  | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
+  | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
          when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 ->
     (match get () with
      | [{CAst.v=(ids,disj_of_patl,b)}] ->
@@ -959,7 +958,7 @@ and factorize_prod scopes vars na bk aty c =
 and factorize_lambda inctx scopes vars na bk aty c =
   let store, get = set_temporary_memory () in
   match na, DAst.get c with
-  | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
+  | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
          when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 ->
     (match get () with
      | [{CAst.v=(ids,disj_of_patl,b)}] ->
@@ -1209,7 +1208,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
   | PIf (c,b1,b2) ->
       GIf (glob_of_pat avoid env sigma c, (Anonymous,None),
            glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2)
-  | PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
+  | PCase ({cip_style=Constr.LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
       let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in
       GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b)
   | PCase (info,p,tm,bl) ->
@@ -1228,7 +1227,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
 	  return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p)
 	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
       in
-      GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
+      GCases (Constr.RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
   | PFix ((ln,i),(lna,tl,bl)) ->
      let def_avoid, def_env, lfi =
        Array.fold_left
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 48f15f897..3a88284e4 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -14,6 +14,7 @@ open Util
 open CAst
 open Names
 open Nameops
+open Constr
 open Namegen
 open Libnames
 open Globnames
@@ -525,7 +526,7 @@ let rec expand_binders ?loc mk bl c =
         let tm = DAst.make ?loc (GVar id) in
         (* Distribute the disjunctive patterns over the shared right-hand side *)
         let eqnl = List.map (fun pat -> CAst.make ?loc (ids,[pat],c)) disjpat in
-        let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in
+        let c = DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in
         expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c)
 
 (**********************************************************************)
@@ -1965,7 +1966,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
                if List.for_all (irrefutable globalenv) thepats then [] else
                   [CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *)
                    DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))]   (* "=> _" *) in
-             Some (DAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
+             Some (DAst.make @@ GCases(RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
 	DAst.make ?loc @@
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 61313acc4..37a327a7d 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -9,7 +9,6 @@ Smartlocate
 Constrexpr_ops
 Ppextend
 Dumpglob
-Topconstr
 Reserve
 Impargs
 Implicit_quantifiers
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 448881dcf..b0480aa70 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -13,6 +13,7 @@ open CErrors
 open Util
 open Names
 open Nameops
+open Constr
 open Globnames
 open Decl_kinds
 open Misctypes
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
deleted file mode 100644
index 7d2d75d9c..000000000
--- a/interp/topconstr.ml
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Constrexpr_ops
-
-let asymmetric_patterns = asymmetric_patterns
-let error_invalid_pattern_notation = error_invalid_pattern_notation
-let split_at_annot = split_at_annot
-let ntn_loc = ntn_loc
-let patntn_loc = patntn_loc
-let map_constr_expr_with_binders = map_constr_expr_with_binders
-let fold_constr_expr_with_binders = fold_constr_expr_with_binders
-let ids_of_cases_indtype = ids_of_cases_indtype
-let occur_var_constr_expr = occur_var_constr_expr
-let free_vars_of_constr_expr = free_vars_of_constr_expr
-let replace_vars_constr_expr = replace_vars_constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
deleted file mode 100644
index c86502015..000000000
--- a/interp/topconstr.mli
+++ /dev/null
@@ -1,53 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-open Constrexpr
-
-(** Topconstr: This whole module is deprecated in favor of Constrexpr_ops  *)
-val asymmetric_patterns : bool ref
-[@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"]
-
-(** Utilities on constr_expr *)
-val split_at_annot : local_binder_expr list -> Misctypes.lident option -> local_binder_expr list * local_binder_expr list
-[@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"]
-
-val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list
-[@@ocaml.deprecated "use Constrexpr_ops.ntn_loc"]
-val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list
-[@@ocaml.deprecated "use Constrexpr_ops.patntn_loc"]
-
-(** For cases pattern parsing errors *)
-val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
-[@@ocaml.deprecated "use Constrexpr_ops.error_invalid_pattern_notation"]
-
-(*************************************************************************)
-val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr
-[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"]
-
-val free_vars_of_constr_expr : constr_expr -> Id.Set.t
-[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"]
-
-val occur_var_constr_expr : Id.t -> constr_expr -> bool
-[@@ocaml.deprecated "use Constrexpr_ops.occur_var_constr_expr"]
-
-(** Specific function for interning "in indtype" syntax of "match" *)
-val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
-[@@ocaml.deprecated "use Constrexpr_ops.ids_of_cases_indtype"]
-
-(** Used in typeclasses *)
-val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) ->
-   ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b
-[@@ocaml.deprecated "use Constrexpr_ops.fold_constr_expr_with_binders"]
-
-val map_constr_expr_with_binders :
-  (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
-      'a -> constr_expr -> constr_expr
-[@@ocaml.deprecated "use Constrexpr_ops.map_constr_expr_with_binders"]