From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- interp/topconstr.mli | 53 ---------------------------------------------------- 1 file changed, 53 deletions(-) delete mode 100644 interp/topconstr.mli (limited to 'interp/topconstr.mli') diff --git a/interp/topconstr.mli b/interp/topconstr.mli deleted file mode 100644 index c8650201..00000000 --- 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 *) -(* 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"] -- cgit v1.2.3