aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/comAssumption.ml12
-rw-r--r--vernac/comAssumption.mli2
-rw-r--r--vernac/comFixpoint.ml8
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/comInductive.ml10
-rw-r--r--vernac/comProgramFixpoint.ml8
-rw-r--r--vernac/indschemes.ml24
-rw-r--r--vernac/indschemes.mli7
-rw-r--r--vernac/lemmas.ml6
-rw-r--r--vernac/metasyntax.ml382
-rw-r--r--vernac/metasyntax.mli5
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/obligations.mli4
-rw-r--r--vernac/proof_using.ml2
-rw-r--r--vernac/record.ml17
-rw-r--r--vernac/record.mli11
-rw-r--r--vernac/vernacentries.ml71
-rw-r--r--vernac/vernacprop.ml12
19 files changed, 307 insertions, 286 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 4a2dba859..695be74bb 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -132,7 +132,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
~program_mode poly ctx (instid, bk, cl) props ?(generalize=true)
?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
- let ((loc, instid), pl) = instid in
+ let ({CAst.loc;v=instid}, pl) = instid in
let sigma, decl = Univdecls.interp_univ_decl_opt env pl in
let tclass, ids =
match bk with
@@ -410,7 +410,7 @@ let context poly l =
let nstatus = match b with
| None ->
pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
- Vernacexpr.NoInline (Loc.tag id))
+ Vernacexpr.NoInline (CAst.make id))
| Some b ->
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~univs ~types:t b in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 5d7adb24a..7e5b941ad 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -42,7 +42,7 @@ let should_axiom_into_instance = function
true
| Global | Local -> !axiom_into_instance
-let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) =
+let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
match local with
| Discharge when Lib.sections_are_opened () ->
let ctx = match ctx with
@@ -109,7 +109,7 @@ let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
let maybe_error_many_udecls = function
- | ((loc,id), Some _) ->
+ | ({CAst.loc;v=id}, Some _) ->
user_err ?loc ~hdr:"many_universe_declarations"
Pp.(str "When declaring multiple axioms in one command, " ++
str "only the first is allowed a universe binder " ++
@@ -126,7 +126,7 @@ let process_assumptions_udecls kind l =
in
let () = match kind, udecl with
| (Discharge, _, _), Some _ when Lib.sections_are_opened () ->
- let loc = fst first_id in
+ let loc = first_id.CAst.loc in
let msg = Pp.str "Section variables cannot be polymorphic." in
user_err ?loc msg
| _ -> ()
@@ -151,8 +151,8 @@ let do_assumptions kind nl l =
let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
let sigma,(t,imps) = interp_assumption sigma env ienv [] c in
let env =
- push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in
- let ienv = List.fold_right (fun (_,id) ienv ->
+ push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in
+ let ienv = List.fold_right (fun {CAst.v=id} ienv ->
let impls = compute_internalization_data env Variable t imps in
Id.Map.add id impls ienv) idl ienv in
((sigma,env,ienv),((is_coe,idl),t,imps)))
@@ -175,7 +175,7 @@ let do_assumptions kind nl l =
let t = replace_vars subst t in
let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
let subst' = List.map2
- (fun (_,id) (c,u) -> (id, Universes.constr_of_global_univ (c,u)))
+ (fun {CAst.v=id} (c,u) -> (id, Universes.constr_of_global_univ (c,u)))
idl refs
in
subst'@subst, status' && status, next_uctx uctx)
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 2fa156abd..0491638c9 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -30,5 +30,5 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
val declare_assumption : coercion_flag -> assumption_kind ->
types in_constant_universes_entry ->
Universes.universe_binders -> Impargs.manual_implicits ->
- bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
+ bool (** implicit *) -> Vernacexpr.inline -> variable CAst.t ->
global_reference * Univ.Instance.t * bool
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index d648e293a..489f299a2 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -102,7 +102,7 @@ let check_mutuality env evd isfix fixl =
type structured_fixpoint_expr = {
fix_name : Id.t;
fix_univs : universe_decl_expr option;
- fix_annot : Id.t Loc.located option;
+ fix_annot : lident option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;
fix_type : constr_expr
@@ -175,7 +175,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
| x , None -> x
| Some ls , Some us ->
let lsu = ls.univdecl_instance and usu = us.univdecl_instance in
- if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then
+ if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then
user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
Some us) fixl None in
let sigma, decl = Univdecls.interp_univ_decl_opt env all_universes in
@@ -323,7 +323,7 @@ let extract_decreasing_argument limit = function
let extract_fixpoint_components limit l =
let fixl, ntnl = List.split l in
- let fixl = List.map (fun (((_,id),pl),ann,bl,typ,def) ->
+ let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) ->
let ann = extract_decreasing_argument limit ann in
{fix_name = id; fix_annot = ann; fix_univs = pl;
fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
@@ -331,7 +331,7 @@ let extract_fixpoint_components limit l =
let extract_cofixpoint_components l =
let fixl, ntnl = List.split l in
- List.map (fun (((_,id),pl),bl,typ,def) ->
+ List.map (fun (({CAst.v=id},pl),bl,typ,def) ->
{fix_name = id; fix_annot = None; fix_univs = pl;
fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
List.flatten ntnl
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 2c84bd84d..2926e30e5 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -31,7 +31,7 @@ val do_cofixpoint :
type structured_fixpoint_expr = {
fix_name : Id.t;
fix_univs : Vernacexpr.universe_decl_expr option;
- fix_annot : Id.t Loc.located option;
+ fix_annot : Misctypes.lident option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;
fix_type : constr_expr
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 41474fc63..c650e9e40 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -249,7 +249,7 @@ let inductive_levels env evd poly arities inds =
(evd,[]) (Array.to_list levels') destarities sizes
in evd, List.rev arities
-let check_named (loc, na) = match na with
+let check_named {CAst.loc;v=na} = match na with
| Name _ -> ()
| Anonymous ->
let msg = str "Parameters must be named." in
@@ -260,7 +260,7 @@ let check_param = function
| CLocalDef (na, _, _) -> check_named na
| CLocalAssum (nas, Default _, _) -> List.iter check_named nas
| CLocalAssum (nas, Generalized _, _) -> ()
-| CLocalPattern (loc,_) ->
+| CLocalPattern {CAst.loc} ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.")
let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
@@ -364,7 +364,7 @@ let eq_local_binders bl1 bl2 =
List.equal local_binder_eq bl1 bl2
let extract_coercions indl =
- let mkqid (_,((_,id),_)) = qualid_of_ident id in
+ let mkqid (_,({CAst.v=id},_)) = qualid_of_ident id in
let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in
List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl))
@@ -378,10 +378,10 @@ let extract_params indl =
params
let extract_inductive indl =
- List.map (fun (((_,indname),pl),_,ar,lc) -> {
+ List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> {
ind_name = indname; ind_univs = pl;
ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar;
- ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
+ ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc
}) indl
let extract_mutual_inductive_declaration_components indl =
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index a9a91e304..af34f8b29 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -298,16 +298,16 @@ let do_program_recursive local poly fixkind fixl ntns =
let do_program_fixpoint local poly l =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
match g, l with
- | [(n, CWfRec r)], [((((_,id),pl),_,bl,typ,def),ntn)] ->
+ | [(n, CWfRec r)], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
let recarg =
match n with
- | Some n -> mkIdentC (snd n)
+ | Some n -> mkIdentC n.CAst.v
| None ->
user_err ~hdr:"do_program_fixpoint"
(str "Recursive argument required for well-founded fixpoints")
in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
- | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] ->
+ | [(n, CMeasureRec (m, r))], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
build_wellfounded (id, pl, n, bl, typ, out_def def) poly
(Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn
@@ -322,7 +322,7 @@ let do_program_fixpoint local poly l =
let extract_cofixpoint_components l =
let fixl, ntnl = List.split l in
- List.map (fun (((_,id),pl),bl,typ,def) ->
+ List.map (fun (({CAst.v=id},pl),bl,typ,def) ->
{fix_name = id; fix_annot = None; fix_univs = pl;
fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
List.flatten ntnl
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 2f4c95aff..447c5085b 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -367,17 +367,16 @@ requested
| InType -> recs ^ "t_nodep")
) in
let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
- let newref = Loc.tag newid in
+ let newref = CAst.make newid in
((newref,isdep,ind,z)::l1),l2
in
match t with
| CaseScheme (x,y,z) -> names "_case" "_case" x y z
| InductionScheme (x,y,z) -> names "_ind" "_rec" x y z
| EqualityScheme x -> l1,((None,smart_global_inductive x)::l2)
-
let do_mutual_induction_scheme lnamedepindsort =
- let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
+ let lrecnames = List.map (fun ({CAst.v},_,_,_) -> v) lnamedepindsort
and env0 = Global.env() in
let sigma, lrecspec, _ =
List.fold_right
@@ -416,7 +415,7 @@ let get_common_underlying_mutual_inductive = function
then user_err Pp.(str "A type occurs twice");
mind,
List.map_filter
- (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all
+ (function (Some id,(_,i)) -> Some (i,id.CAst.v) | (None,_) -> None) all
let do_scheme l =
let ischeme,escheme = split_scheme l in
@@ -450,7 +449,7 @@ let fold_left' f = function
let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ())
let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ())
-
+
let build_combined_scheme env schemes =
let evdref = ref (Evd.from_env env) in
let defs = List.map (fun cst ->
@@ -492,18 +491,19 @@ let build_combined_scheme env schemes =
(!evdref, body, typ)
let do_combined_scheme name schemes =
+ let open CAst in
let csts =
- List.map (fun x ->
- let refe = Ident x in
- let qualid = qualid_of_reference refe in
- try Nametab.locate_constant (snd qualid)
- with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared."))
+ List.map (fun {CAst.loc;v} ->
+ let refe = Ident (Loc.tag ?loc v) in
+ let qualid = qualid_of_reference refe in
+ try Nametab.locate_constant (snd qualid)
+ with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared."))
schemes
in
let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
- ignore (define (snd name) UserIndividualRequest sigma proof_output (Some typ));
- fixpoint_message None [snd name]
+ ignore (define name.v UserIndividualRequest sigma proof_output (Some typ));
+ fixpoint_message None [name.v]
(**********************************************************************)
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index 4b31389ab..8658d85f6 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
open Names
open Constr
open Environ
@@ -31,17 +30,17 @@ val declare_rewriting_schemes : inductive -> unit
(** Mutual Minimality/Induction scheme *)
val do_mutual_induction_scheme :
- (Id.t located * bool * inductive * Sorts.family) list -> unit
+ (Misctypes.lident * bool * inductive * Sorts.family) list -> unit
(** Main calls to interpret the Scheme command *)
-val do_scheme : (Id.t located option * scheme) list -> unit
+val do_scheme : (Misctypes.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 : Id.t located -> Id.t located list -> unit
+val do_combined_scheme : Misctypes.lident -> Misctypes.lident list -> unit
(** Hook called at each inductive type definition *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 57436784b..7661fff6d 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -214,7 +214,7 @@ let fresh_name_for_anonymous_theorem () =
let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
next_global_ident_away default_thm_id avoid
-let check_name_freshness locality (loc,id) : unit =
+let check_name_freshness locality {CAst.loc;v=id} : unit =
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
@@ -339,7 +339,7 @@ let universe_proof_terminator compute_guard hook =
(hook (Some (proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
- | Some (_,id) -> save_anonymous ~export_seff proof id
+ | Some { CAst.v = id } -> save_anonymous ~export_seff proof id
end
end
@@ -444,7 +444,7 @@ let start_proof_com ?inference_hook kind thms hook =
let ids = List.map RelDecl.get_name ctx in
check_name_freshness (pi1 kind) id;
(* XXX: The nf_evar is critical !! *)
- evd, (snd id,
+ evd, (id.CAst.v,
(Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
(ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
evd thms in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 3be357598..f63206216 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -43,13 +43,6 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
let entry_buf = Buffer.create 64
-type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry
-
-let grammars : any_entry list String.Map.t ref = ref String.Map.empty
-
-let register_grammar name grams =
- grammars := String.Map.add name grams !grammars
-
let pr_entry e =
let () = Buffer.clear entry_buf in
let ft = Format.formatter_of_buffer entry_buf in
@@ -57,11 +50,11 @@ let pr_entry e =
str (Buffer.contents entry_buf)
let pr_registered_grammar name =
- let gram = try Some (String.Map.find name !grammars) with Not_found -> None in
+ let gram = try Some (Pcoq.find_grammars_by_name name) with Not_found -> None in
match gram with
| None -> user_err Pp.(str "Unknown or unprintable grammar entry.")
| Some entries ->
- let pr_one (AnyEntry e) =
+ let pr_one (Pcoq.AnyEntry e) =
str "Entry " ++ str (Pcoq.Gram.Entry.name e) ++ str " is" ++ fnl () ++
pr_entry e
in
@@ -96,7 +89,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 ((loc, str) : lstring) =
+let parse_format ({CAst.loc;v=str} : Misctypes.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
@@ -199,36 +192,6 @@ let parse_format ((loc, str) : lstring) =
(***********************)
(* Analyzing notations *)
-type symbol_token = WhiteSpace of int | String of string
-
-let split_notation_string str =
- let push_token beg i l =
- if Int.equal beg i then l else
- let s = String.sub str beg (i - beg) in
- String s :: l
- in
- let push_whitespace beg i l =
- if Int.equal beg i then l else WhiteSpace (i-beg) :: l
- in
- let rec loop beg i =
- if i < String.length str then
- if str.[i] == ' ' then
- push_token beg i (loop_on_whitespace (i+1) (i+1))
- else
- loop beg (i+1)
- else
- push_token beg i []
- and loop_on_whitespace beg i =
- if i < String.length str then
- if str.[i] != ' ' then
- push_whitespace beg i (loop i (i+1))
- else
- loop_on_whitespace beg (i+1)
- else
- push_whitespace beg i []
- in
- loop 0 0
-
(* Interpret notations with a recursive component *)
let out_nt = function NonTerminal x -> x | _ -> assert false
@@ -284,17 +247,6 @@ let quote_notation_token x =
if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'"
else x
-let rec raw_analyze_notation_tokens = function
- | [] -> []
- | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl
- | String "_" :: _ -> user_err Pp.(str "_ must be quoted.")
- | String x :: sl when CLexer.is_ident x ->
- NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl
- | String s :: sl ->
- Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl
- | WhiteSpace n :: sl ->
- Break n :: raw_analyze_notation_tokens sl
-
let is_numeral symbs =
match List.filter (function Break _ -> false | _ -> true) symbs with
| ([Terminal "-"; Terminal x] | [Terminal x]) ->
@@ -315,8 +267,8 @@ let rec get_notation_vars onlyprint = function
| (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl
| SProdList _ :: _ -> assert false
-let analyze_notation_tokens ~onlyprint l =
- let l = raw_analyze_notation_tokens l in
+let analyze_notation_tokens ~onlyprint ntn =
+ let l = decompose_raw_notation ntn in
let vars = get_notation_vars onlyprint l in
let recvars,l = interp_list_parser [] l in
recvars, List.subtract Id.equal vars (List.map snd recvars), l
@@ -333,13 +285,17 @@ let prec_assoc = function
| LeftA -> (E,L)
| NonA -> (L,L)
-let precedence_of_entry_type from = function
- | ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n
- | ETConstr (NumLevel n,BorderProd (b,Some a)) ->
+let precedence_of_position_and_level from = function
+ | NumLevel n, BorderProd (_,None) -> n, Prec n
+ | NumLevel n, BorderProd (b,Some a) ->
n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
- | ETConstr (NumLevel n,InternalProd) -> n, Prec n
- | ETConstr (NextLevel,_) -> from, L
- | _ -> 0, E (* ?? *)
+ | NumLevel n, InternalProd -> n, Prec n
+ | NextLevel, _ -> from, L
+
+let precedence_of_entry_type from = function
+ | ETConstr x | ETConstrAsBinder (_,x) -> precedence_of_position_and_level from x
+ | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n
+ | _ -> 0, E (* should not matter *)
(* Some breaking examples *)
(* "x = y" : "x /1 = y" (breaks before any symbol) *)
@@ -377,8 +333,8 @@ let is_non_terminal = function
| NonTerminal _ | SProdList _ -> true
| _ -> false
-let is_next_non_terminal = function
-| [] -> false
+let is_next_non_terminal b = function
+| [] -> b
| pr :: _ -> is_non_terminal pr
let is_next_terminal = function Terminal _ :: _ -> true | _ -> false
@@ -387,8 +343,9 @@ let is_next_break = function Break _ :: _ -> true | _ -> false
let add_break n l = (None,UnpCut (PpBrk(n,0))) :: l
-let add_break_if_none n = function
- | (((_,UnpCut (PpBrk _)) :: _) | []) as l -> l
+let add_break_if_none n b = function
+ | (_,UnpCut (PpBrk _)) :: _ as l -> l
+ | [] when not b -> []
| l -> (None,UnpCut (PpBrk(n,0))) :: l
let check_open_binder isopen sl m =
@@ -403,45 +360,59 @@ let check_open_binder isopen sl m =
prlist_with_sep spc pr_token sl
++ strbrk "\" is allowed to occur.")
+let unparsing_metavar i from typs =
+ let x = List.nth typs (i-1) in
+ let prec = snd (precedence_of_entry_type from x) in
+ match x with
+ | ETConstr _ | ETConstrAsBinder _ | ETReference | ETBigint ->
+ UnpMetaVar (i,prec)
+ | ETPattern _ ->
+ UnpBinderMetaVar (i,prec)
+ | ETName ->
+ UnpBinderMetaVar (i,Prec 0)
+ | ETBinder isopen ->
+ assert false
+ | ETOther _ -> failwith "TODO"
+
(* Heuristics for building default printing rules *)
let index_id id l = List.index Id.equal id l
let make_hunks etyps symbols from =
let vars,typs = List.split etyps in
- let rec make = function
+ let rec make b = function
| NonTerminal m :: prods ->
let i = index_id m vars in
- let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
- let u = UnpMetaVar (i,prec) in
- if is_next_non_terminal prods then
- (None,u) :: add_break_if_none 1 (make prods)
+ let u = unparsing_metavar i from typs in
+ if is_next_non_terminal b prods then
+ (None, u) :: add_break_if_none 1 b (make b prods)
else
- (None,u) :: make_with_space prods
- | Terminal s :: prods when List.exists is_non_terminal prods ->
+ (None, u) :: make_with_space b prods
+ | Terminal s :: prods
+ when (* true to simulate presence of non-terminal *) b || List.exists is_non_terminal prods ->
if (is_comma s || is_operator s) then
(* Always a breakable space after comma or separator *)
- (None,UnpTerminal s) :: add_break_if_none 1 (make prods)
+ (None, UnpTerminal s) :: add_break_if_none 1 b (make b prods)
else if is_right_bracket s && is_next_terminal prods then
(* Always no space after right bracked, but possibly a break *)
- (None,UnpTerminal s) :: add_break_if_none 0 (make prods)
- else if is_left_bracket s && is_next_non_terminal prods then
- (None,UnpTerminal s) :: make prods
+ (None, UnpTerminal s) :: add_break_if_none 0 b (make b prods)
+ else if is_left_bracket s && is_next_non_terminal b prods then
+ (None, UnpTerminal s) :: make b prods
else if not (is_next_break prods) then
(* Add rigid space, no break, unless user asked for something *)
- (None,UnpTerminal (s^" ")) :: make prods
+ (None, UnpTerminal (s^" ")) :: make b prods
else
(* Rely on user spaces *)
- (None,UnpTerminal s) :: make prods
+ (None, UnpTerminal s) :: make b prods
| Terminal s :: prods ->
(* Separate but do not cut a trailing sequence of terminal *)
(match prods with
- | Terminal _ :: _ -> (None,UnpTerminal (s^" ")) :: make prods
- | _ -> (None,UnpTerminal s) :: make prods)
+ | Terminal _ :: _ -> (None,UnpTerminal (s^" ")) :: make b prods
+ | _ -> (None,UnpTerminal s) :: make b prods)
| Break n :: prods ->
- add_break n (make prods)
+ add_break n (make b prods)
| SProdList (m,sl) :: prods ->
let i = index_id m vars in
@@ -451,47 +422,52 @@ let make_hunks etyps symbols from =
(* If no separator: add a break *)
if List.is_empty sl then add_break 1 []
(* We add NonTerminal for simulation but remove it afterwards *)
- else snd (List.sep_last (make (sl@[NonTerminal m]))) in
+ else make true sl in
let hunk = match typ with
| ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl')
| ETBinder isopen ->
check_open_binder isopen sl m;
UnpBinderListMetaVar (i,isopen,List.map snd sl')
| _ -> assert false in
- (None,hunk) :: make_with_space prods
+ (None, hunk) :: make_with_space b prods
| [] -> []
- and make_with_space prods =
+ and make_with_space b prods =
match prods with
| Terminal s' :: prods'->
if is_operator s' then
(* A rigid space before operator and a breakable after *)
- (None,UnpTerminal (" "^s')) :: add_break_if_none 1 (make prods')
+ (None,UnpTerminal (" "^s')) :: add_break_if_none 1 b (make b prods')
else if is_comma s' then
(* No space whatsoever before comma *)
- make prods
+ make b prods
else if is_right_bracket s' then
- make prods
+ make b prods
else
(* A breakable space between any other two terminals *)
- add_break_if_none 1 (make prods)
+ add_break_if_none 1 b (make b prods)
| (NonTerminal _ | SProdList _) :: _ ->
(* A breakable space before a non-terminal *)
- add_break_if_none 1 (make prods)
+ add_break_if_none 1 b (make b prods)
| Break _ :: _ ->
(* Rely on user wish *)
- make prods
+ make b prods
| [] -> []
- in make symbols
+ in make false symbols
(* Build default printing rules from explicit format *)
let error_format ?loc () = user_err ?loc Pp.(str "The format does not match the notation.")
+let warn_format_break =
+ CWarnings.create ~name:"notation-both-format-and-spaces" ~category:"parsing"
+ (fun () ->
+ strbrk "Discarding format implicitly indicated by multiple spaces in notation because an explicit format modifier is given.")
+
let rec split_format_at_ldots hd = function
- | (loc,UnpTerminal s) :: fmt when String.equal s (Id.to_string ldots_var) -> loc, List.rev hd, fmt
+ | (loc,UnpTerminal s) :: fmt when String.equal s (Id.to_string Notation_ops.ldots_var) -> loc, List.rev hd, fmt
| u :: fmt ->
check_no_ldots_in_box u;
split_format_at_ldots (u::hd) fmt
@@ -538,8 +514,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
| NonTerminal s :: symbs, (_,UnpTerminal s') :: fmt when Id.equal s (Id.of_string s') ->
let i = index_id s vars in
- let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
- let symbs, l = aux (symbs,fmt) in symbs, UnpMetaVar (i,prec) :: l
+ let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from typs :: l
| symbs, (_,UnpBox (a,b)) :: fmt ->
let symbs', b' = aux (symbs,b) in
let symbs', l = aux (symbs',fmt) in
@@ -562,6 +537,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
| _ -> assert false in
symbs, hunk :: l
| symbs, [] -> symbs, []
+ | Break _ :: symbs, fmt -> warn_format_break (); aux (symbs,fmt)
| _, fmt -> error_format ?loc:(fst (List.hd fmt)) ()
in
match aux symfmt with
@@ -574,8 +550,8 @@ let hunks_of_format (from,(vars,typs)) symfmt =
let assoc_of_type n (_,typ) = precedence_of_entry_type n typ
let is_not_small_constr = function
- ETConstr _ -> true
- | ETOther("constr","binder_constr") -> true
+ ETProdConstr _ -> true
+ | ETProdOther("constr","binder_constr") -> true
| _ -> false
let rec define_keywords_aux = function
@@ -607,14 +583,14 @@ let distribute a ll = List.map (fun l -> a @ l) ll
let expand_list_rule typ tkl x n p ll =
let camlp5_message_name = Some (add_suffix x ("_"^string_of_int n)) in
- let main = GramConstrNonTerminal (ETConstr typ, camlp5_message_name) in
+ let main = GramConstrNonTerminal (ETProdConstr typ, camlp5_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 (p+n,true,p) :: hds
- @ [GramConstrNonTerminal (ETConstrList (typ,tkl), Some x)] in
+ @ [GramConstrNonTerminal (ETProdConstrList (typ,tkl), Some x)] in
distribute hds ll
else
distribute (GramConstrListMark (i+1,false,p) :: hds @ [main]) ll @
@@ -623,7 +599,7 @@ let expand_list_rule typ tkl x n p ll =
let is_constr_typ typ x etyps =
match List.assoc x etyps with
- | ETConstr typ' -> typ = typ'
+ | ETConstr typ' | ETConstrAsBinder (_,typ') -> typ = typ'
| _ -> false
let include_possible_similar_trailing_pattern typ etyps sl l =
@@ -636,12 +612,21 @@ let include_possible_similar_trailing_pattern typ etyps sl l =
with Exit -> n,l in
try_aux 0 l
+let prod_entry_type = function
+ | ETName -> ETProdName
+ | ETReference -> ETProdReference
+ | ETBigint -> ETProdBigint
+ | ETBinder _ -> assert false (* See check_binder_type *)
+ | ETConstr p | ETConstrAsBinder (_,p) -> ETProdConstr p
+ | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n)
+ | ETOther (s,t) -> ETProdOther (s,t)
+
let make_production etyps symbols =
let rec aux = function
| [] -> [[]]
| NonTerminal m :: l ->
let typ = List.assoc m etyps in
- distribute [GramConstrNonTerminal (typ, Some m)] (aux l)
+ distribute [GramConstrNonTerminal (prod_entry_type typ, Some m)] (aux l)
| Terminal s :: l ->
distribute [GramConstrTerminal (CLexer.terminal s)] (aux l)
| Break _ :: l ->
@@ -656,8 +641,10 @@ let make_production etyps symbols =
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)
+ check_open_binder o sl x;
+ let typ = if o then (assert (tkl = []); ETBinderOpen) else ETBinderClosed tkl in
+ distribute
+ [GramConstrNonTerminal (ETProdBinderList typ, 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
@@ -675,6 +662,7 @@ let rec find_symbols c_current c_next c_last = function
let border = function
| (_,ETConstr(_,BorderProd (_,a))) :: _ -> a
+ | (_,(ETConstrAsBinder(_,(_,BorderProd (_,a))))) :: _ -> a
| _ -> None
let recompute_assoc typs =
@@ -688,17 +676,16 @@ let recompute_assoc typs =
(* Registration of syntax extensions (parsing/printing, no interpretation)*)
let pr_arg_level from (lev,typ) =
- let pplev = match lev with
+ let pplev = function
| (n,L) when Int.equal n from -> str "at next level"
| (n,E) -> str "at level " ++ int n
| (n,L) -> str "at level below " ++ int n
| (n,Prec m) when Int.equal m n -> str "at level " ++ int n
| (n,_) -> str "Unknown level" in
- let pptyp = match typ with
- | NtnInternTypeConstr -> mt ()
- | NtnInternTypeBinder -> str " " ++ surround (str "binder")
- | NtnInternTypeIdent -> str " " ++ surround (str "ident") in
- pplev ++ pptyp
+ Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
+ (match typ with
+ | ETConstr _ | ETConstrAsBinder _ | ETPattern _ -> spc () ++ pplev lev
+ | _ -> mt ())
let pr_level ntn (from,args,typs) =
str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
@@ -802,7 +789,7 @@ type notation_modifier = {
only_parsing : bool;
only_printing : bool;
compat : Flags.compat_version option;
- format : string Loc.located option;
+ format : Misctypes.lstring option;
extra : (string * string) list;
}
@@ -830,15 +817,23 @@ let interp_modifiers modl = let open NotationMods in
interp { acc with etyps = (id,typ) :: acc.etyps; } l
| SetItemLevel ([],n) :: l ->
interp acc l
+ | SetItemLevelAsBinder ([],_,_) :: l ->
+ interp acc l
| SetItemLevel (s::idl,n) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id acc.etyps then
user_err ~hdr:"Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
- let typ = ETConstr (n,()) in
+ let typ = ETConstr (Some n) in
interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevel (idl,n)::l)
+ | SetItemLevelAsBinder (s::idl,bk,n) :: l ->
+ let id = Id.of_string s in
+ if Id.List.mem_assoc id acc.etyps then
+ user_err ~hdr:"Metasyntax.interp_modifiers"
+ (str s ++ str " is already assigned to an entry or constr level.");
+ let typ = ETConstrAsBinder (bk,n) in
+ interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevelAsBinder (idl,bk,n)::l)
| SetLevel n :: l ->
-
interp { acc with level = Some n; } l
| SetAssoc a :: l ->
if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once.");
@@ -852,7 +847,7 @@ let interp_modifiers modl = let open NotationMods in
| SetFormat ("text",s) :: l ->
if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
interp { acc with format = Some s; } l
- | SetFormat (k,(_,s)) :: l ->
+ | SetFormat (k,{CAst.v=s}) :: l ->
interp { acc with extra = (k,s)::acc.extra; } l
in interp default modl
@@ -902,12 +897,17 @@ let get_compat_version mods =
let set_entry_type etyps (x,typ) =
let typ = try
match List.assoc x etyps, typ with
- | ETConstr (n,()), (_,BorderProd (left,_)) ->
+ | ETConstr (Some n), (_,BorderProd (left,_)) ->
ETConstr (n,BorderProd (left,None))
- | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
- | (ETPattern | ETName | ETBigint | ETOther _ |
- ETReference | ETBinder _ as t), _ -> t
- | (ETBinderList _ |ETConstrList _), _ -> assert false
+ | ETConstr (Some n), (_,InternalProd) -> ETConstr (n,InternalProd)
+ | ETConstrAsBinder (bk, Some n), (_,BorderProd (left,_)) ->
+ ETConstrAsBinder (bk, (n,BorderProd (left,None)))
+ | ETConstrAsBinder (bk, Some n), (_,InternalProd) ->
+ ETConstrAsBinder (bk, (n,InternalProd))
+ | ETPattern (b,n), _ -> ETPattern (b,n)
+ | (ETName | ETBigint | ETReference | ETBinder _ | ETOther _ as x), _ -> x
+ | ETConstr None, _ -> ETConstr typ
+ | ETConstrAsBinder (bk,None), _ -> ETConstrAsBinder (bk,typ)
with Not_found -> ETConstr typ
in (x,typ)
@@ -927,12 +927,9 @@ let join_auxiliary_recursive_types recvars etyps =
recvars etyps
let internalization_type_of_entry_type = function
- | ETConstr _ -> NtnInternTypeConstr
- | ETBigint | ETReference -> NtnInternTypeConstr
- | ETBinder _ -> NtnInternTypeBinder
- | ETName -> NtnInternTypeIdent
- | ETPattern | ETOther _ -> user_err Pp.(str "Not supported.")
- | ETBinderList _ | ETConstrList _ -> assert false
+ | ETBinder _ -> NtnInternTypeOnlyBinder
+ | ETConstr _ | ETConstrAsBinder _ | ETBigint | ETReference
+ | ETName | ETPattern _ | ETOther _ -> NtnInternTypeAny
let set_internalization_type typs =
List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
@@ -943,28 +940,36 @@ let make_internalization_vars recvars mainvars typs =
maintyps @ extratyps
let make_interpretation_type isrec isonlybinding = function
- | NtnInternTypeConstr when isrec -> NtnTypeConstrList
- | NtnInternTypeConstr | NtnInternTypeIdent ->
- if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr
- | NtnInternTypeBinder when isrec -> NtnTypeBinderList
- | NtnInternTypeBinder -> user_err Pp.(str "Type binder is only for use in recursive notations for binders.")
-
-let make_interpretation_vars recvars allvars =
+ | ETConstr _ ->
+ if isrec then NtnTypeConstrList else
+ if isonlybinding then
+ (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *)
+ NtnTypeBinder (NtnBinderParsedAsConstr AsIdent)
+ else NtnTypeConstr
+ | ETConstrAsBinder (bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk)
+ | ETName -> NtnTypeBinder NtnParsedAsIdent
+ | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *)
+ | ETBigint | ETReference | ETOther _ -> NtnTypeConstr
+ | ETBinder _ ->
+ if isrec then NtnTypeBinderList
+ else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
+
+let make_interpretation_vars recvars allvars typs =
let eq_subscope (sc1, l1) (sc2, l2) =
Option.equal String.equal sc1 sc2 &&
List.equal String.equal l1 l2
in
let check (x, y) =
- let (_,scope1, _) = Id.Map.find x allvars in
- let (_,scope2, _) = Id.Map.find y allvars in
+ let (_,scope1) = Id.Map.find x allvars in
+ let (_,scope2) = Id.Map.find y allvars in
if not (eq_subscope scope1 scope2) then error_not_same_scope x y
in
let () = List.iter check recvars in
let useless_recvars = List.map snd recvars in
let mainvars =
Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in
- Id.Map.mapi (fun x (isonlybinding, sc, typ) ->
- (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
+ Id.Map.mapi (fun x (isonlybinding, sc) ->
+ (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding (Id.List.assoc x typs))) mainvars
let check_rule_productivity l =
if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
@@ -979,18 +984,27 @@ let warn_notation_bound_to_variable =
let warn_non_reversible_notation =
CWarnings.create ~name:"non-reversible-notation" ~category:"parsing"
- (fun () ->
- strbrk "This notation will not be used for printing as it is not reversible.")
-
-let is_not_printable onlyparse nonreversible = function
+ (function
+ | APrioriReversible -> assert false
+ | HasLtac ->
+ strbrk "This notation contains Ltac expressions: it will not be used for printing."
+ | NonInjective ids ->
+ let n = List.length ids in
+ strbrk (String.plural n "Variable") ++ spc () ++ pr_enum Id.print ids ++ spc () ++
+ strbrk (if n > 1 then "do" else "does") ++
+ str " not occur in the right-hand side." ++ spc() ++
+ strbrk "The notation will not be used for printing as it is not reversible.")
+
+let is_not_printable onlyparse reversibility = function
| NVar _ ->
if not onlyparse then warn_notation_bound_to_variable ();
true
| _ ->
- if not onlyparse && nonreversible then
- (warn_non_reversible_notation (); true)
+ if not onlyparse && reversibility <> APrioriReversible then
+ (warn_non_reversible_notation reversibility; true)
else onlyparse
+
let find_precedence lev etyps symbols onlyprint =
let first_symbol =
let rec aux = function
@@ -1008,29 +1022,30 @@ let find_precedence lev etyps symbols onlyprint =
match first_symbol with
| None -> [],0
| Some (NonTerminal x) ->
+ let test () =
+ if onlyprint then
+ if Option.is_empty lev then
+ user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.")
+ else [],Option.get lev
+ else
+ user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
(try match List.assoc x etyps with
- | ETConstr _ ->
- if onlyprint then
- if Option.is_empty lev then
- user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.")
- else [],Option.get lev
- else
- user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.")
- | ETName | ETBigint | ETReference ->
+ | ETConstr _ -> test ()
+ | ETConstrAsBinder (_,Some _) -> test ()
+ | (ETName | ETBigint | ETReference) ->
begin match lev with
| None ->
([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
| Some 0 ->
([],0)
| _ ->
- user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
+ user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
end
- | ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *)
- if Option.is_empty lev then
- user_err Pp.(str "Need an explicit level.")
- else [],Option.get lev
- | ETConstrList _ | ETBinderList _ ->
- assert false (* internally used in grammar only *)
+ | (ETPattern _ | ETBinder _ | ETOther _ | ETConstrAsBinder _) ->
+ (* Give a default ? *)
+ if Option.is_empty lev then
+ user_err Pp.(str "Need an explicit level.")
+ else [],Option.get lev
with Not_found ->
if Option.is_empty lev then
user_err Pp.(str "A left-recursive notation must have an explicit level.")
@@ -1074,7 +1089,7 @@ let remove_curly_brackets l =
module SynData = struct
- type subentry_types = (Id.t * (production_level, production_position) constr_entry_key_gen) list
+ type subentry_types = (Id.t * (production_level * production_position) constr_entry_key_gen) list
(* XXX: Document *)
type syn_data = {
@@ -1086,7 +1101,7 @@ module SynData = struct
only_parsing : bool;
only_printing : bool;
compat : Flags.compat_version option;
- format : string Loc.located option;
+ format : Misctypes.lstring option;
extra : (string * string) list;
(* XXX: Callback to printing, must remove *)
@@ -1128,8 +1143,7 @@ let compute_syntax_data df modifiers =
let onlyparse = mods.only_parsing in
if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
let assoc = Option.append mods.assoc (Some NonA) in
- let toks = split_notation_string df in
- let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint toks in
+ let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
let _ = check_useless_entry_types recvars mainvars mods.etyps in
let _ = check_binder_type recvars mods.etyps in
@@ -1152,7 +1166,7 @@ let compute_syntax_data df modifiers =
let i_typs = set_internalization_type sy_typs in
let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in
let pp_sy_data = (sy_typs,symbols) in
- let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,i_typs),need_squash) in
+ let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,List.map snd sy_typs_for_grammar),need_squash) in
let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
let i_data = ntn_for_interp, df' in
@@ -1171,7 +1185,7 @@ let compute_syntax_data df modifiers =
mainvars;
intern_typs = i_typs;
- level = (n,prec,i_typs);
+ level = (n,prec,List.map snd sy_typs);
pa_syntax_data = pa_sy_data;
pp_syntax_data = pp_sy_data;
not_data = sy_fulldata;
@@ -1329,10 +1343,10 @@ let add_notation_in_scope local df env c mods scope =
ninterp_var_type = to_map i_vars;
ninterp_rec_vars = to_map sd.recvars;
} in
- let (acvars, ac, reversible) = interp_notation_constr env nenv c in
- let interp = make_interpretation_vars sd.recvars acvars in
+ let (acvars, ac, reversibility) = interp_notation_constr env nenv c in
+ let interp = make_interpretation_vars sd.recvars acvars (fst sd.pa_syntax_data) in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
- let onlyparse = is_not_printable sd.only_parsing (not reversible) ac in
+ let onlyparse = is_not_printable sd.only_parsing reversibility ac in
let notation = {
notobj_local = local;
notobj_scope = scope;
@@ -1350,8 +1364,7 @@ let add_notation_in_scope local df env c mods scope =
sd.info
let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
- let dfs = split_notation_string df in
- let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in
+ let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
let i_typs, onlyprint = if not (is_numeral symbs) then begin
let sy = recover_notation_syntax (make_notation_key symbs) in
@@ -1363,15 +1376,15 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
(* Declare interpretation *)
let path = (Lib.library_dp(), Lib.current_dirpath true) in
let df' = (make_notation_key symbs, (path,df)) in
- let i_vars = make_internalization_vars recvars mainvars i_typs in
+ let i_vars = make_internalization_vars recvars mainvars (List.map internalization_type_of_entry_type i_typs) in
let nenv = {
ninterp_var_type = to_map i_vars;
ninterp_rec_vars = to_map recvars;
} in
- let (acvars, ac, reversible) = interp_notation_constr env ~impls nenv c in
- let interp = make_interpretation_vars recvars acvars in
+ let (acvars, ac, reversibility) = interp_notation_constr env ~impls nenv c in
+ let interp = make_interpretation_vars recvars acvars (List.combine mainvars i_typs) in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
- let onlyparse = is_not_printable onlyparse (not reversible) ac in
+ let onlyparse = is_not_printable onlyparse reversibility ac in
let notation = {
notobj_local = local;
notobj_scope = scope;
@@ -1387,7 +1400,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
(* Notations without interpretation (Reserved Notation) *)
-let add_syntax_extension local ((loc,df),mods) = let open SynData in
+let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in
let psd = compute_pure_syntax_data df mods in
let sy_rules = make_syntax_rules {psd with compat = None} in
Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs;
@@ -1395,11 +1408,11 @@ let add_syntax_extension local ((loc,df),mods) = let open SynData in
(* Notations with only interpretation *)
-let add_notation_interpretation env ((loc,df),c,sc) =
+let add_notation_interpretation env ({CAst.loc;v=df},c,sc) =
let df' = add_notation_interpretation_core false df env c sc false false None in
Dumpglob.dump_notation (loc,df') sc true
-let set_notation_for_interpretation env impls ((_,df),c,sc) =
+let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) =
(try ignore
(Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ());
with NoSyntaxRule ->
@@ -1408,7 +1421,7 @@ let set_notation_for_interpretation env impls ((_,df),c,sc) =
(* Main entry point *)
-let add_notation local env c ((loc,df),modifiers) sc =
+let add_notation local env c ({CAst.loc;v=df},modifiers) sc =
let df' =
if no_syntax_modifiers modifiers then
(* No syntax data: try to rely on a previously declared rule *)
@@ -1427,8 +1440,7 @@ let add_notation local env c ((loc,df),modifiers) sc =
let add_notation_extra_printing_rule df k v =
let notk =
- let dfs = split_notation_string df in
- let _,_, symbs = analyze_notation_tokens ~onlyprint:true dfs in
+ let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in
make_notation_key symbs in
Notation.add_notation_extra_printing_rule notk k v
@@ -1436,13 +1448,13 @@ let add_notation_extra_printing_rule df k v =
let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None)
-let add_infix local env ((loc,inf),modifiers) pr sc =
+let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
check_infix_modifiers modifiers;
(* check the precedence *)
let metas = [inject_var "x"; inject_var "y"] in
let c = mkAppC (pr,metas) in
- let df = "x "^(quote_notation_token inf)^" y" in
- add_notation local env c ((loc,df),modifiers) sc
+ let df = CAst.make ?loc @@ "x "^(quote_notation_token inf)^" y" in
+ add_notation local env c (df,modifiers) sc
(**********************************************************************)
(* Delimiters and classes bound to scopes *)
@@ -1499,23 +1511,21 @@ let try_interp_name_alias = function
| _ -> raise Not_found
let add_syntactic_definition env ident (vars,c) local onlyparse =
- let nonprintable = ref false in
- let vars,pat =
- try [], NRef (try_interp_name_alias (vars,c))
+ let vars,reversibility,pat =
+ try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
with Not_found ->
- let fold accu id = Id.Map.add id NtnInternTypeConstr accu in
+ let fold accu id = Id.Map.add id NtnInternTypeAny accu in
let i_vars = List.fold_left fold Id.Map.empty vars in
let nenv = {
ninterp_var_type = i_vars;
ninterp_rec_vars = Id.Map.empty;
} in
- let nvars, pat, reversible = interp_notation_constr env nenv c in
- let () = nonprintable := not reversible in
- let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in
- List.map map vars, pat
+ let nvars, pat, reversibility = interp_notation_constr env nenv c in
+ let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
+ List.map map vars, reversibility, pat
in
let onlyparse = match onlyparse with
- | None when (is_not_printable false !nonprintable pat) -> Some Flags.Current
+ | None when (is_not_printable false reversibility pat) -> Some Flags.Current
| p -> p
in
Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index e064b570e..7740604c3 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -12,6 +12,7 @@ open Notation
open Constrexpr
open Notation_term
open Environ
+open Misctypes
val add_token_obj : string -> unit
@@ -55,10 +56,6 @@ val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
val pr_grammar : string -> Pp.t
-type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry
-
-val register_grammar : string -> any_entry list -> unit
-
val check_infix_modifiers : syntax_modifier list -> unit
val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 58e4b00fc..e4bcbc4bb 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -295,10 +295,10 @@ type obligation =
type obligations = (obligation array * int)
type fixpoint_kind =
- | IsFixpoint of (Id.t Loc.located option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list
| IsCoFixpoint
-type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+type notations = (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type program_info_aux = {
prg_name: Id.t;
@@ -500,7 +500,7 @@ let rec lam_index n t acc =
let compute_possible_guardness_evidences (n,_) fixbody fixtype =
match n with
- | Some (loc, n) -> [lam_index n fixbody 0]
+ | Some { CAst.loc; v = n } -> [lam_index n fixbody 0]
| None ->
(* If recursive argument was not given by user, we try all args.
An earlier approach was to look only for inductive arguments,
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index bdc97d48c..0ec127152 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -61,10 +61,10 @@ val add_definition : Names.Id.t -> ?term:constr -> types ->
?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
type notations =
- (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+ (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type fixpoint_kind =
- | IsFixpoint of (Id.t Loc.located option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list
| IsCoFixpoint
val add_mutual_definitions :
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index ffe99cfd8..8422baf57 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -51,7 +51,7 @@ let rec process_expr env e ty =
let rec aux = function
| SsEmpty -> Id.Set.empty
| SsType -> set_of_type env ty
- | SsSingl (_,id) -> set_of_id env id
+ | SsSingl { CAst.v = id } -> set_of_id env id
| SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
| SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
| SsCompl e -> Id.Set.diff (full_set env) (aux e)
diff --git a/vernac/record.ml b/vernac/record.ml
index 16b95a5ef..1140e3d37 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -62,7 +62,7 @@ let _ =
let interp_fields_evars env sigma impls_env nots l =
List.fold_left2
- (fun (env, sigma, uimpls, params, impls) no ((loc, i), b, t) ->
+ (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) ->
let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in
let sigma, b' =
Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
@@ -92,8 +92,9 @@ let compute_constructor_level evars env l =
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:(fst n) @@ CHole (None, Misctypes.IntroAnonymous, None))
+ | 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))
let binders_of_decls = List.map binder_of_decl
@@ -101,7 +102,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
let env0 = Global.env () in
let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in
let _ =
- let error bk (loc, name) =
+ let error bk {CAst.loc; v=name} =
match bk, name with
| Default _, Anonymous ->
user_err ?loc ~hdr:"record" (str "Record parameters must be named")
@@ -110,7 +111,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
List.iter
(function CLocalDef (b, _, _) -> error default_binder_kind b
| CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
- | CLocalPattern (loc,(_,_)) ->
+ | CLocalPattern {CAst.loc} ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
in
let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in
@@ -571,13 +572,13 @@ open Vernacexpr
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
or subinstances. *)
-let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
+let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl)),ps,cfs,idbuild,s) =
let cfs,notations = List.split cfs in
let cfs,priorities = List.split cfs in
let coers,fs = List.split cfs in
let extract_name acc = function
- Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
- | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
+ Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc
+ | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc
| _ -> acc in
let allnames = idstruc::(List.fold_left extract_name [] fs) in
let () = match List.duplicates Id.equal allnames with
diff --git a/vernac/record.mli b/vernac/record.mli
index e632e7bbf..e0a4b8fdd 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -13,6 +13,17 @@ open Globnames
val primitive_flag : bool ref
+val declare_projections :
+ inductive ->
+ Entries.constant_universes_entry ->
+ ?kind:Decl_kinds.definition_object_kind ->
+ Id.t ->
+ bool list ->
+ Universes.universe_binders ->
+ Impargs.manual_implicits list ->
+ Context.Rel.t ->
+ (Name.t * bool) list * Constant.t option list
+
val definition_structure :
inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ca904d50b..4613100fc 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -10,6 +10,7 @@
open Pp
open CErrors
+open CAst
open Util
open Names
open Nameops
@@ -443,11 +444,13 @@ let start_proof_and_print k l hook =
let hook env sigma ev =
let tac = !Obligations.default_tactic in
let evi = Evd.find sigma ev in
+ let evi = Evarutil.nf_evar_info sigma evi in
let env = Evd.evar_filtered_env evi in
try
- let concl = Evarutil.nf_evars_universes sigma evi.Evd.evar_concl in
- let concl = EConstr.of_constr concl in
- if Evarutil.has_undefined_evars sigma concl then raise Exit;
+ let concl = EConstr.of_constr evi.Evd.evar_concl in
+ if not (Evarutil.is_ground_env sigma env &&
+ Evarutil.is_ground_term sigma concl)
+ then raise Exit;
let c, _, ctx =
Pfedit.build_by_tactic env (Evd.evar_universe_context sigma)
concl (Tacticals.New.tclCOMPLETE tac)
@@ -469,13 +472,13 @@ let vernac_definition_hook p = function
| SubClass -> Class.add_subclass_hook p
| _ -> no_hook
-let vernac_definition ~atts discharge kind ((loc, id), pl) def =
+let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
let local = enforce_locality_exp atts.locality discharge in
let hook = vernac_definition_hook atts.polymorphic kind in
let () =
match id with
| Anonymous -> ()
- | Name n -> let lid = (loc, n) in
+ | Name n -> let lid = CAst.make ?loc n in
match local with
| Discharge -> Dumpglob.dump_definition lid true "var"
| Local | Global -> Dumpglob.dump_definition lid false "def"
@@ -489,7 +492,7 @@ let vernac_definition ~atts discharge kind ((loc, id), pl) def =
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
- [((loc, name), pl), (bl, t)] hook
+ [(CAst.make ?loc name, pl), (bl, t)] hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
| None -> None
@@ -544,14 +547,14 @@ let should_treat_as_cumulative cum poly =
let vernac_record cum k poly finite struc binders sort nameopt cfs =
let is_cumulative = should_treat_as_cumulative cum poly in
let const = match nameopt with
- | None -> add_prefix "Build_" (snd (fst (snd struc)))
- | Some (_,id as lid) ->
+ | None -> add_prefix "Build_" (fst (snd struc)).v
+ | Some ({v=id} as lid) ->
Dumpglob.dump_definition lid false "constr"; id in
if Dumpglob.dump () then (
Dumpglob.dump_definition (fst (snd struc)) false "rec";
List.iter (fun (((_, x), _), _) ->
match x with
- | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
+ | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> Dumpglob.dump_definition (make ?loc id) false "proj"
| _ -> ()) cfs);
ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort))
@@ -580,9 +583,9 @@ let vernac_inductive ~atts cum lo finite indl =
atts.polymorphic finite id bl c oc fs
| [ ( id , bl , c , Class _, Constructors [l]), [] ] ->
let f =
- let (coe, ((loc, id), ce)) = l in
+ let (coe, ({loc;v=id}, ce)) = l in
let coe' = if coe then Some true else None in
- (((coe', AssumExpr ((loc, Name id), ce)), None), [])
+ (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), [])
in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f]
| [ ( _ , _, _, Class _, Constructors _), [] ] ->
user_err Pp.(str "Inductive classes not supported")
@@ -635,7 +638,7 @@ let vernac_scheme l =
let vernac_combined_scheme lid l =
if Dumpglob.dump () then
(Dumpglob.dump_definition lid false "def";
- List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l);
+ List.iter (fun {loc;v=id} -> dump_global (Misctypes.AN (Ident (Loc.tag ?loc id)))) l);
Indschemes.do_combined_scheme lid l
let vernac_universe ~atts l =
@@ -658,7 +661,7 @@ let vernac_constraint ~atts l =
let vernac_import export refl =
Library.import_module export (List.map qualid_of_reference refl)
-let vernac_declare_module export (loc, id) binders_ast mty_ast =
+let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
if Lib.sections_are_opened () then
@@ -676,7 +679,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export
-let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
+let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
if Lib.sections_are_opened () then
@@ -687,7 +690,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
- (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast
+ (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast
([],[]) in
let mp =
Declaremods.start_module Modintern.interp_module_ast
@@ -717,13 +720,13 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)])
export
-let vernac_end_module export (loc,id as lid) =
+let vernac_end_module export {loc;v=id} =
let mp = Declaremods.end_module () in
Dumpglob.dump_modref ?loc mp "mod";
Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
- Option.iter (fun export -> vernac_import export [Ident lid]) export
+ Option.iter (fun export -> vernac_import export [Ident (Loc.tag ?loc id)]) export
-let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
+let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
if Lib.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
@@ -733,7 +736,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
- (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast
+ (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast
([],[]) in
let mp =
@@ -763,7 +766,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
Flags.if_verbose Feedback.msg_info
(str "Module Type " ++ Id.print id ++ str " is defined")
-let vernac_end_modtype (loc,id) =
+let vernac_end_modtype {loc;v=id} =
let mp = Declaremods.end_modtype () in
Dumpglob.dump_modref ?loc mp "modtype";
Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined")
@@ -776,21 +779,21 @@ let vernac_include l =
(* Sections *)
-let vernac_begin_section (_, id as lid) =
+let vernac_begin_section ({v=id} as lid) =
Proof_global.check_no_pending_proof ();
Dumpglob.dump_definition lid true "sec";
Lib.open_section id
-let vernac_end_section (loc,_) =
+let vernac_end_section {CAst.loc} =
Dumpglob.dump_reference ?loc
(DirPath.to_string (Lib.current_dirpath true)) "<>" "sec";
Lib.close_section ()
-let vernac_name_sec_hyp (_,id) set = Proof_using.name_set id set
+let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set
(* Dispatcher of the "End" command *)
-let vernac_end_segment (_,id as lid) =
+let vernac_end_segment ({v=id} as lid) =
Proof_global.check_no_pending_proof ();
match Lib.find_opening_node id with
| Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
@@ -973,7 +976,7 @@ let vernac_hints ~atts lb h =
let vernac_syntactic_definition ~atts lid x y =
Dumpglob.dump_definition lid false "syndef";
let local = enforce_module_locality atts.locality in
- Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y
+ Metasyntax.add_syntactic_definition (Global.env()) lid.v x local y
let vernac_declare_implicits ~atts r l =
let local = make_section_locality atts.locality in
@@ -1209,7 +1212,7 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
end;
if scopes_specified || clear_scopes_flag then begin
- let scopes = List.map (Option.map (fun (loc,k) ->
+ let scopes = List.map (Option.map (fun {loc;v=k} ->
try ignore (Notation.find_scope k); k
with UserError _ ->
Notation.find_delimiters_scope ?loc k)) scopes
@@ -1830,7 +1833,7 @@ let vernac_locate = function
let vernac_register id r =
if Proof_global.there_are_pending_proofs () then
user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
- let kn = Constrintern.global_reference (snd id) in
+ let kn = Constrintern.global_reference id.v in
if not (isConstRef kn) then
user_err Pp.(str "Register inline: a constant is expected");
match r with
@@ -2021,7 +2024,7 @@ let interp ?proof ~atts ~st c =
| VernacImport (export,qidl) -> vernac_import export qidl
| VernacCanonical qid -> vernac_canonical qid
| VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t
- | VernacIdentityCoercion ((_,id),s,t) ->
+ | VernacIdentityCoercion ({v=id},s,t) ->
vernac_identity_coercion ~atts id s t
(* Type classes *)
@@ -2239,12 +2242,12 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
aux ~polymorphism ~atts v
| VernacFail v -> with_fail st true (fun () -> control v)
| VernacTimeout (n,v) ->
- current_timeout := Some n;
- control v
- | VernacRedirect (s, (_,v)) ->
- Topfmt.with_output_to_file s control v
- | VernacTime (batch, (_loc,v)) ->
- System.with_time ~batch control v;
+ current_timeout := Some n;
+ control v
+ | VernacRedirect (s, {v}) ->
+ Topfmt.with_output_to_file s control v
+ | VernacTime (batch, {v}) ->
+ System.with_time ~batch control v;
and aux ~polymorphism ~atts : _ -> unit =
function
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 3932d1c7b..172a20b7a 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -13,15 +13,15 @@ open Vernacexpr
let rec under_control = function
| VernacExpr (_, c) -> c
- | VernacRedirect (_,(_,c))
- | VernacTime (_,(_,c))
+ | VernacRedirect (_,{CAst.v=c})
+ | VernacTime (_,{CAst.v=c})
| VernacFail c
| VernacTimeout (_,c) -> under_control c
let rec has_Fail = function
| VernacExpr _ -> false
- | VernacRedirect (_,(_,c))
- | VernacTime (_,(_,c))
+ | VernacRedirect (_,{CAst.v=c})
+ | VernacTime (_,{CAst.v=c})
| VernacTimeout (_,c) -> has_Fail c
| VernacFail _ -> true
@@ -38,8 +38,8 @@ let is_navigation_vernac c =
is_navigation_vernac_expr (under_control c)
let rec is_deep_navigation_vernac = function
- | VernacTime (_,(_,c)) -> is_deep_navigation_vernac c
- | VernacRedirect (_, (_,c))
+ | VernacTime (_,{CAst.v=c}) -> is_deep_navigation_vernac c
+ | VernacRedirect (_, {CAst.v=c})
| VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
| VernacExpr _ -> false
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 00:04:59 +0000