aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml3
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/comFixpoint.ml1
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/egramcoq.ml2
-rw-r--r--vernac/g_proofs.ml42
-rw-r--r--vernac/g_vernac.ml49
-rw-r--r--vernac/indschemes.mli6
-rw-r--r--vernac/metasyntax.ml6
-rw-r--r--vernac/metasyntax.mli1
-rw-r--r--vernac/misctypes.ml75
-rw-r--r--vernac/obligations.ml4
-rw-r--r--vernac/obligations.mli4
-rw-r--r--vernac/ppvernac.ml2
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernac.mllib2
-rw-r--r--vernac/vernacentries.ml3
-rw-r--r--vernac/vernacentries.mli4
-rw-r--r--vernac/vernacexpr.ml1
19 files changed, 103 insertions, 30 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 8b56275c7..ee578669c 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -24,7 +24,8 @@ open Globnames
open Inductiveops
open Tactics
open Ind_tables
-open Misctypes
+open Namegen
+open Tactypes
open Proofview.Notations
module RelDecl = Context.Rel.Declaration
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 946a7bb32..8cf3895fb 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -145,7 +145,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
(fun avoid (clname, _) ->
match clname with
| Some cl ->
- let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in
+ let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
t, avoid
| None -> failwith ("new instance: under-applied typeclass"))
cl
@@ -255,7 +255,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
k.cl_projs;
c :: props, rest'
with Not_found ->
- ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest
+ ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
else props, rest)
([], props) k.cl_props
in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index b5b8697d2..1d1cc62de 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -13,7 +13,6 @@ open Decl_kinds
open Pretyping
open Evarutil
open Evarconv
-open Misctypes
module RelDecl = Context.Rel.Declaration
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a6992a30b..f51bfbad5 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -33,7 +33,7 @@ val do_cofixpoint :
type structured_fixpoint_expr = {
fix_name : Id.t;
fix_univs : Constrexpr.universe_decl_expr option;
- fix_annot : Misctypes.lident option;
+ fix_annot : lident option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;
fix_type : constr_expr
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index e7a308dda..434e836d8 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -228,7 +228,7 @@ type _ target =
type prod_info = production_level * production_position
type (_, _) entry =
-| TTName : ('self, Misctypes.lname) entry
+| TTName : ('self, lname) entry
| TTReference : ('self, reference) entry
| TTBigint : ('self, Constrexpr.raw_natural_number) entry
| TTConstr : prod_info * 'r target -> ('r, 'r) entry
diff --git a/vernac/g_proofs.ml4 b/vernac/g_proofs.ml4
index a3806ff68..4b11276af 100644
--- a/vernac/g_proofs.ml4
+++ b/vernac/g_proofs.ml4
@@ -8,10 +8,10 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+open Glob_term
open Constrexpr
open Vernacexpr
open Proof_global
-open Misctypes
open Pcoq
open Pcoq.Prim
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index b6523981c..3a59242de 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -12,6 +12,7 @@ open Pp
open CErrors
open Util
open Names
+open Glob_term
open Vernacexpr
open Constrexpr
open Constrexpr_ops
@@ -19,7 +20,7 @@ open Extend
open Decl_kinds
open Declaremods
open Declarations
-open Misctypes
+open Namegen
open Tok (* necessary for camlp5 *)
open Pcoq
@@ -338,7 +339,7 @@ GEXTEND Gram
;
type_cstr:
[ [ ":"; c=lconstr -> c
- | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ]
+ | -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) ] ]
;
(* Inductive schemes *)
scheme:
@@ -394,7 +395,7 @@ GEXTEND Gram
(None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ]
;
record_binder:
- [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))
+ [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))
| id = name; f = record_binder_body -> f id ] ]
;
assum_list:
@@ -413,7 +414,7 @@ GEXTEND Gram
t= [ coe = of_type_with_opt_coercion; c = lconstr ->
fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c))
| ->
- fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ]
+ fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))) ]
-> t l
]]
;
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index bd4249cac..261c3d813 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -32,17 +32,17 @@ val declare_rewriting_schemes : inductive -> unit
(** Mutual Minimality/Induction scheme *)
val do_mutual_induction_scheme :
- (Misctypes.lident * bool * inductive * Sorts.family) list -> unit
+ (lident * bool * inductive * Sorts.family) list -> unit
(** Main calls to interpret the Scheme command *)
-val do_scheme : (Misctypes.lident option * scheme) list -> unit
+val do_scheme : (lident option * scheme) list -> unit
(** Combine a list of schemes into a conjunction of them *)
val build_combined_scheme : env -> Constant.t list -> Evd.evar_map * constr * types
-val do_combined_scheme : Misctypes.lident -> Misctypes.lident list -> unit
+val do_combined_scheme : lident -> lident list -> unit
(** Hook called at each inductive type definition *)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 2245e762f..8f64f5519 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -92,7 +92,7 @@ let pr_grammar = function
(* Parse a format (every terminal starting with a letter or a single
quote (except a single quote alone) must be quoted) *)
-let parse_format ({CAst.loc;v=str} : Misctypes.lstring) =
+let parse_format ({CAst.loc;v=str} : lstring) =
let len = String.length str in
(* TODO: update the line of the location when the string contains newlines *)
let make_loc i j = Option.map (Loc.shift_loc (i+1) (j-len)) loc in
@@ -792,7 +792,7 @@ type notation_modifier = {
only_parsing : bool;
only_printing : bool;
compat : Flags.compat_version option;
- format : Misctypes.lstring option;
+ format : lstring option;
extra : (string * string) list;
}
@@ -1104,7 +1104,7 @@ module SynData = struct
only_parsing : bool;
only_printing : bool;
compat : Flags.compat_version option;
- format : Misctypes.lstring option;
+ format : lstring option;
extra : (string * string) list;
(* XXX: Callback to printing, must remove *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index a6c12e089..f6de75b07 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -14,7 +14,6 @@ open Notation
open Constrexpr
open Notation_term
open Environ
-open Misctypes
val add_token_obj : string -> unit
diff --git a/vernac/misctypes.ml b/vernac/misctypes.ml
new file mode 100644
index 000000000..ae725efaa
--- /dev/null
+++ b/vernac/misctypes.ml
@@ -0,0 +1,75 @@
+(* Compat module, to be removed in 8.10 *)
+open Names
+
+type lident = Names.lident
+[@@ocaml.deprecated "use [Names.lident"]
+type lname = Names.lname
+[@@ocaml.deprecated "use [Names.lname]"]
+type lstring = Names.lstring
+[@@ocaml.deprecated "use [Names.lstring]"]
+
+type 'a or_by_notation_r = 'a Constrexpr.or_by_notation_r =
+ | AN of 'a [@ocaml.deprecated "use version in [Constrexpr]"]
+ | ByNotation of (string * string option) [@ocaml.deprecated "use version in [Constrexpr]"]
+[@@ocaml.deprecated "use [Constrexpr.or_by_notation_r]"]
+
+type 'a or_by_notation = 'a Constrexpr.or_by_notation
+[@@ocaml.deprecated "use [Constrexpr.or_by_notation]"]
+
+type intro_pattern_naming_expr = Namegen.intro_pattern_naming_expr =
+ | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Evarutil]"]
+ | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Evarutil]"]
+ | IntroAnonymous [@ocaml.deprecated "Use version in [Evarutil]"]
+[@@ocaml.deprecated "use [Evarutil.intro_pattern_naming_expr]"]
+
+type 'a or_var = 'a Locus.or_var =
+ | ArgArg of 'a [@ocaml.deprecated "Use version in [Locus]"]
+ | ArgVar of Names.lident [@ocaml.deprecated "Use version in [Locus]"]
+[@@ocaml.deprecated "use [Locus.or_var]"]
+
+type quantified_hypothesis = Tactypes.quantified_hypothesis =
+ AnonHyp of int [@ocaml.deprecated "Use version in [Tactypes]"]
+ | NamedHyp of Id.t [@ocaml.deprecated "Use version in [Tactypes]"]
+[@@ocaml.deprecated "use [Tactypes.quantified_hypothesis]"]
+
+type multi = Equality.multi =
+ | Precisely of int [@ocaml.deprecated "use version in [Equality]"]
+ | UpTo of int [@ocaml.deprecated "use version in [Equality]"]
+ | RepeatStar [@ocaml.deprecated "use version in [Equality]"]
+ | RepeatPlus [@ocaml.deprecated "use version in [Equality]"]
+[@@ocaml.deprecated "use [Equality.multi]"]
+
+type 'a bindings = 'a Tactypes.bindings =
+ | ImplicitBindings of 'a list [@ocaml.deprecated "use version in [Tactypes]"]
+ | ExplicitBindings of 'a Tactypes.explicit_bindings [@ocaml.deprecated "use version in [Tactypes]"]
+ | NoBindings [@ocaml.deprecated "use version in [Tactypes]"]
+[@@ocaml.deprecated "use [Tactypes.bindings]"]
+
+type 'constr intro_pattern_expr = 'constr Tactypes.intro_pattern_expr =
+ | IntroForthcoming of bool [@ocaml.deprecated "use version in [Tactypes]"]
+ | IntroNaming of Namegen.intro_pattern_naming_expr [@ocaml.deprecated "use version in [Tactypes]"]
+ | IntroAction of 'constr Tactypes.intro_pattern_action_expr [@ocaml.deprecated "use version in [Tactypes]"]
+and 'constr intro_pattern_action_expr = 'constr Tactypes.intro_pattern_action_expr =
+ | IntroWildcard [@ocaml.deprecated "use [Tactypes]"]
+ | IntroOrAndPattern of 'constr Tactypes.or_and_intro_pattern_expr [@ocaml.deprecated "use [Tactypes]"]
+ | IntroInjection of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"]
+ | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t [@ocaml.deprecated "use [Tactypes]"]
+ | IntroRewrite of bool [@ocaml.deprecated "use [Tactypes]"]
+and 'constr or_and_intro_pattern_expr = 'constr Tactypes.or_and_intro_pattern_expr =
+ | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list [@ocaml.deprecated "use [Tactypes]"]
+ | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"]
+[@@ocaml.deprecated "use version in [Tactypes]"]
+
+type 'id move_location = 'id Logic.move_location =
+ | MoveAfter of 'id [@ocaml.deprecated "use version in [Logic]"]
+ | MoveBefore of 'id [@ocaml.deprecated "use version in [Logic]"]
+ | MoveFirst [@ocaml.deprecated "use version in [Logic]"]
+ | MoveLast [@ocaml.deprecated "use version in [Logic]"]
+[@@ocaml.deprecated "use version in [Logic]"]
+
+type 'a cast_type = 'a Glob_term.cast_type =
+ | CastConv of 'a [@ocaml.deprecated "use version in [Glob_term]"]
+ | CastVM of 'a [@ocaml.deprecated "use version in [Glob_term]"]
+ | CastCoerce [@ocaml.deprecated "use version in [Glob_term]"]
+ | CastNative of 'a [@ocaml.deprecated "use version in [Glob_term]"]
+[@@ocaml.deprecated "use version in [Glob_term]"]
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 00f1760c2..1ab24b670 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -298,10 +298,10 @@ type obligation =
type obligations = (obligation array * int)
type fixpoint_kind =
- | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
| IsCoFixpoint
-type notations = (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type program_info_aux = {
prg_name: Id.t;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index b1eaf51ac..a37c30aaf 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -62,10 +62,10 @@ val add_definition : Names.Id.t -> ?term:constr -> types ->
?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
type notations =
- (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+ (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type fixpoint_kind =
- | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
| IsCoFixpoint
val add_mutual_definitions :
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 5490b9ce5..d0c423650 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -286,7 +286,7 @@ open Pputils
prlist_strict (pr_module_vardecls pr_c) l
let pr_type_option pr_c = function
- | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt()
+ | { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt()
| _ as c -> brk(0,2) ++ str" :" ++ pr_c c
let pr_decl_notation prc ({loc; v=ntn},c,scopt) =
diff --git a/vernac/record.ml b/vernac/record.ml
index e6a3afe4e..940859723 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -96,7 +96,7 @@ let binder_of_decl = function
| Vernacexpr.AssumExpr(n,t) -> (n,None,t)
| Vernacexpr.DefExpr(n,c,t) ->
(n,Some c, match t with Some c -> c
- | None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Misctypes.IntroAnonymous, None))
+ | None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Namegen.IntroAnonymous, None))
let binders_of_decls = List.map binder_of_decl
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 39c313ac7..356951b69 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -31,3 +31,5 @@ Vernacstate
Mltop
Topfmt
Vernacentries
+
+Misctypes
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7f6270df1..94eb45fd3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -29,7 +29,6 @@ open Decl_kinds
open Constrexpr
open Redexpr
open Lemmas
-open Misctypes
open Locality
open Vernacinterp
@@ -637,7 +636,7 @@ let vernac_scheme l =
let vernac_combined_scheme lid l =
if Dumpglob.dump () then
(Dumpglob.dump_definition lid false "def";
- List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Misctypes.AN (make ?loc @@ Ident id))) l);
+ List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (make ?loc @@ Ident id))) l);
Indschemes.do_combined_scheme lid l
let vernac_universe ~atts l =
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f6199e820..3c88a3443 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -8,9 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Misctypes
-
-val dump_global : Libnames.reference or_by_notation -> unit
+val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit
(** Vernacular entries *)
val vernac_require :
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 9e8dfc4f8..5acac9e25 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Misctypes
open Constrexpr
open Libnames
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 01:15:35 +0000