aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml5
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/explainErr.mli6
-rw-r--r--vernac/himsg.mli21
-rw-r--r--vernac/indschemes.ml8
-rw-r--r--vernac/metasyntax.ml95
-rw-r--r--vernac/metasyntax.mli2
-rw-r--r--vernac/mltop.mli6
-rw-r--r--vernac/obligations.ml10
-rw-r--r--vernac/obligations.mli5
-rw-r--r--vernac/record.ml7
-rw-r--r--vernac/topfmt.mli8
-rw-r--r--vernac/vernacentries.ml4
13 files changed, 102 insertions, 77 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 86bbf46a35..6711b14da0 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -311,10 +311,7 @@ let traverse current t =
(** Hopefully bullet-proof function to recover the type of a constant. It just
ignores all the universe stuff. There are many issues that can arise when
considering terms out of any valid environment, so use with caution. *)
-let type_of_constant cb = match cb.Declarations.const_type with
-| Declarations.RegularArity ty -> ty
-| Declarations.TemplateArity (ctx, arity) ->
- Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level)
+let type_of_constant cb = cb.Declarations.const_type
let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
let (idts, knst) = st in
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 793a4c580f..2178a7caa0 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -18,7 +18,7 @@ let guill s = str "\"" ++ str s ++ str "\""
(** Invariant : exceptions embedded in EvaluatedError satisfy
Errors.noncritical *)
-exception EvaluatedError of std_ppcmds * exn option
+exception EvaluatedError of Pp.t * exn option
(** Registration of generic errors
Nota: explain_exn does NOT end with a newline anymore!
diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli
index 944339d851..0cbd71fa4f 100644
--- a/vernac/explainErr.mli
+++ b/vernac/explainErr.mli
@@ -7,7 +7,7 @@
(************************************************************************)
(** Toplevel Exception *)
-exception EvaluatedError of Pp.std_ppcmds * exn option
+exception EvaluatedError of Pp.t * exn option
(** Pre-explain a vernac interpretation error *)
@@ -16,6 +16,6 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn
(** General explain function. Should not be used directly now,
see instead function [Errors.print] and variants *)
-val explain_exn_default : exn -> Pp.std_ppcmds
+val explain_exn_default : exn -> Pp.t
-val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option Loc.located) option) -> unit
+val register_additional_error_info : (Util.iexn -> (Pp.t option Loc.located) option) -> unit
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index b95ef8425a..5b91f9e682 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Indtypes
open Environ
open Type_errors
@@ -18,28 +17,28 @@ open Logic
(** This module provides functions to explain the type errors. *)
-val explain_type_error : env -> Evd.evar_map -> type_error -> std_ppcmds
+val explain_type_error : env -> Evd.evar_map -> type_error -> Pp.t
-val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> std_ppcmds
+val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t
-val explain_inductive_error : inductive_error -> std_ppcmds
+val explain_inductive_error : inductive_error -> Pp.t
-val explain_typeclass_error : env -> typeclass_error -> Pp.std_ppcmds
+val explain_typeclass_error : env -> typeclass_error -> Pp.t
-val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds
+val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t
-val explain_refiner_error : refiner_error -> std_ppcmds
+val explain_refiner_error : refiner_error -> Pp.t
val explain_pattern_matching_error :
- env -> Evd.evar_map -> pattern_matching_error -> std_ppcmds
+ env -> Evd.evar_map -> pattern_matching_error -> Pp.t
val explain_reduction_tactic_error :
- Tacred.reduction_tactic_error -> std_ppcmds
+ Tacred.reduction_tactic_error -> Pp.t
-val explain_module_error : Modops.module_typing_error -> std_ppcmds
+val explain_module_error : Modops.module_typing_error -> Pp.t
val explain_module_internalization_error :
- Modintern.module_internalization_error -> std_ppcmds
+ Modintern.module_internalization_error -> Pp.t
val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 3d97a767c8..6ea8bc7f2c 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,13 +109,17 @@ let _ =
let define id internal ctx c t =
let f = declare_constant ~internal in
+ let _, univs = Evd.universe_context ctx in
+ let univs =
+ if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
+ else Monomorphic_const_entry univs
+ in
let kn = f id
(DefinitionEntry
{ const_entry_body = c;
const_entry_secctx = None;
const_entry_type = t;
- const_entry_polymorphic = Flags.is_universe_polymorphism ();
- const_entry_universes = snd (Evd.universe_context ctx);
+ const_entry_universes = univs;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 567fc57fae..c0974d0a7c 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -615,46 +615,71 @@ let define_keywords = function
let distribute a ll = List.map (fun l -> a @ l) ll
- (* Expand LIST1(t,sep) into the combination of t and t;sep;LIST1(t,sep)
- as many times as expected in [n] argument *)
-let rec expand_list_rule typ tkl x n i hds ll =
- if Int.equal i n then
+ (* Expand LIST1(t,sep);sep;t;...;t (with the trailing pattern
+ occurring p times, possibly p=0) into the combination of
+ t;sep;t;...;t;sep;t (p+1 times)
+ t;sep;t;...;t;sep;t;sep;t (p+2 times)
+ ...
+ t;sep;t;...;t;sep;t;...;t;sep;t (p+n times)
+ t;sep;t;...;t;sep;t;...;t;sep;t;LIST1(t,sep) *)
+
+let expand_list_rule typ tkl x n p ll =
+ let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in
+ let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in
+ let tks = List.map (fun x -> GramConstrTerminal x) tkl in
+ let rec aux i hds ll =
+ if i < p then aux (i+1) (main :: tks @ hds) ll
+ else if Int.equal i (p+n) then
let hds =
- GramConstrListMark (n,true) :: hds
+ GramConstrListMark (p+n,true,p) :: hds
@ [GramConstrNonTerminal (ETConstrList (typ,tkl), Some x)] in
distribute hds ll
else
- let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in
- let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in
- let tks = List.map (fun x -> GramConstrTerminal x) tkl in
- distribute (GramConstrListMark (i+1,false) :: hds @ [main]) ll @
- expand_list_rule typ tkl x n (i+1) (main :: tks @ hds) ll
+ distribute (GramConstrListMark (i+1,false,p) :: hds @ [main]) ll @
+ aux (i+1) (main :: tks @ hds) ll in
+ aux 0 [] ll
+
+let is_constr_typ typ x etyps =
+ match List.assoc x etyps with
+ | ETConstr typ' -> typ = typ'
+ | _ -> false
+
+let include_possible_similar_trailing_pattern typ etyps sl l =
+ let rec aux n = function
+ | Terminal s :: sl, Terminal s'::l' when s = s' -> aux n (sl,l')
+ | [], NonTerminal x ::l' when is_constr_typ typ x etyps -> try_aux n l'
+ | _ -> raise Exit
+ and try_aux n l =
+ try aux (n+1) (sl,l)
+ with Exit -> n,l in
+ try_aux 0 l
let make_production etyps symbols =
- let prod =
- List.fold_right
- (fun t ll -> match t with
- | NonTerminal m ->
- let typ = List.assoc m etyps in
- distribute [GramConstrNonTerminal (typ, Some m)] ll
- | Terminal s ->
- distribute [GramConstrTerminal (CLexer.terminal s)] ll
- | Break _ ->
- ll
- | SProdList (x,sl) ->
- let tkl = List.flatten
- (List.map (function Terminal s -> [CLexer.terminal s]
- | Break _ -> []
- | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in
- match List.assoc x etyps with
- | ETConstr typ -> expand_list_rule typ tkl x 1 0 [] ll
- | ETBinder o ->
- distribute
- [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll
- | _ ->
- user_err Pp.(str "Components of recursive patterns in notation must be terms or binders."))
- symbols [[]] in
- List.map define_keywords prod
+ let rec aux = function
+ | [] -> [[]]
+ | NonTerminal m :: l ->
+ let typ = List.assoc m etyps in
+ distribute [GramConstrNonTerminal (typ, Some m)] (aux l)
+ | Terminal s :: l ->
+ distribute [GramConstrTerminal (CLexer.terminal s)] (aux l)
+ | Break _ :: l ->
+ aux l
+ | SProdList (x,sl) :: l ->
+ let tkl = List.flatten
+ (List.map (function Terminal s -> [CLexer.terminal s]
+ | Break _ -> []
+ | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in
+ match List.assoc x etyps with
+ | ETConstr typ ->
+ let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in
+ expand_list_rule typ tkl x 1 p (aux l')
+ | ETBinder o ->
+ distribute
+ [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] (aux l)
+ | _ ->
+ user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.") in
+ let prods = aux symbols in
+ List.map define_keywords prods
let rec find_symbols c_current c_next c_last = function
| [] -> []
@@ -1056,7 +1081,7 @@ module SynData = struct
extra : (string * string) list;
(* XXX: Callback to printing, must remove *)
- msgs : ((std_ppcmds -> unit) * std_ppcmds) list;
+ msgs : ((Pp.t -> unit) * Pp.t) list;
(* Fields for internalization *)
recvars : (Id.t * Id.t) list;
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index c9e37a4eb2..9cd00cbcb4 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -52,7 +52,7 @@ val add_syntactic_definition : Id.t -> Id.t list * constr_expr ->
(** Print the Camlp4 state of a grammar *)
-val pr_grammar : string -> Pp.std_ppcmds
+val pr_grammar : string -> Pp.t
type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index 3ecda656df..324a66d382 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -83,6 +83,6 @@ val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
(** {5 Utilities} *)
-val print_ml_path : unit -> Pp.std_ppcmds
-val print_ml_modules : unit -> Pp.std_ppcmds
-val print_gc : unit -> Pp.std_ppcmds
+val print_ml_path : unit -> Pp.t
+val print_ml_modules : unit -> Pp.t
+val print_gc : unit -> Pp.t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 10d3317f8d..28aeaa725e 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -636,12 +636,12 @@ let declare_obligation prg obl body ty uctx =
shrink_body body ty else [], body, ty, [||]
in
let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+ let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in
let ce =
{ const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
const_entry_secctx = None;
const_entry_type = ty;
- const_entry_polymorphic = poly;
- const_entry_universes = uctx;
+ const_entry_universes = univs;
const_entry_opaque = opaque;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -818,8 +818,7 @@ let solve_by_tac name evi t poly ctx =
id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
let env = Global.env () in
let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
- let body, eff = Future.force entry.const_entry_body in
- assert(Safe_typing.empty_private_constants = eff);
+ let body, () = Future.force entry.const_entry_body in
let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
Inductiveops.control_only_guard (Global.env ()) (fst body);
(fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
@@ -836,8 +835,7 @@ let obligation_terminator name num guard hook auto pf =
let env = Global.env () in
let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
let ty = entry.Entries.const_entry_type in
- let (body, cstr), eff = Future.force entry.Entries.const_entry_body in
- assert(Safe_typing.empty_private_constants = eff);
+ let (body, cstr), () = Future.force entry.Entries.const_entry_body in
let sigma = Evd.from_ctx (fst uctx) in
let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
Inductiveops.control_only_guard (Global.env ()) body;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index fa691ad1b6..5614403ba5 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -10,7 +10,6 @@ open Environ
open Term
open Evd
open Names
-open Pp
open Globnames
(* This is a hack to make it possible for Obligations to craft a Qed
@@ -96,12 +95,12 @@ val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option ->
val show_obligations : ?msg:bool -> Names.Id.t option -> unit
-val show_term : Names.Id.t option -> std_ppcmds
+val show_term : Names.Id.t option -> Pp.t
val admit_obligations : Names.Id.t option -> unit
exception NoObligations of Names.Id.t option
-val explain_no_obligations : Names.Id.t option -> Pp.std_ppcmds
+val explain_no_obligations : Names.Id.t option -> Pp.t
val set_program_mode : bool -> unit
diff --git a/vernac/record.ml b/vernac/record.ml
index 63ca227862..a2e443e5f7 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -322,13 +322,16 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
try
+ let univs =
+ if poly then Polymorphic_const_entry ctx
+ else Monomorphic_const_entry ctx
+ in
let entry = {
const_entry_body =
Future.from_val (Safe_typing.mk_pure_proof proj);
const_entry_secctx = None;
const_entry_type = Some projtyp;
- const_entry_polymorphic = poly;
- const_entry_universes = ctx;
+ const_entry_universes = univs;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None } in
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 6e006fc6c9..afe76f6f87 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -37,8 +37,8 @@ val set_margin : int option -> unit
val get_margin : unit -> int option
(** Console display of feedback, we may add some location information *)
-val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
-val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
+val std_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit
+val emacs_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit
(** Color output *)
val clear_styles : unit -> unit
@@ -51,8 +51,8 @@ val init_terminal_output : color:bool -> unit
(** Error printing *)
(* To be deprecated when we can fully move to feedback-based error
printing. *)
-val pr_loc : Loc.t -> Pp.std_ppcmds
-val print_err_exn : ?extra:Pp.std_ppcmds -> exn -> unit
+val pr_loc : Loc.t -> Pp.t
+val print_err_exn : ?extra:Pp.t -> exn -> unit
(** [with_output_to_file file f x] executes [f x] with logging
redirected to a file [file] *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9650ea19d7..959df89f6e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -257,7 +257,7 @@ let print_namespace ns =
in
let print_constant k body =
(* FIXME: universes *)
- let t = Typeops.type_of_constant_type (Global.env ()) body.Declarations.const_type in
+ let t = body.Declarations.const_type in
print_kn k ++ str":" ++ spc() ++ Printer.pr_type t
in
let matches mp = match match_modulepath ns mp with
@@ -2120,7 +2120,7 @@ let locate_if_not_already ?loc (e, info) =
| Some l -> (e, info)
exception HasNotFailed
-exception HasFailed of std_ppcmds
+exception HasFailed of Pp.t
let with_fail b f =
if not b then f ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 06:03:29 +0000