diff options
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/classes.ml | 4 | ||||
-rw-r--r-- | vernac/comAssumption.ml | 12 | ||||
-rw-r--r-- | vernac/comAssumption.mli | 2 | ||||
-rw-r--r-- | vernac/comFixpoint.ml | 8 | ||||
-rw-r--r-- | vernac/comFixpoint.mli | 2 | ||||
-rw-r--r-- | vernac/comInductive.ml | 10 | ||||
-rw-r--r-- | vernac/comProgramFixpoint.ml | 8 | ||||
-rw-r--r-- | vernac/indschemes.ml | 24 | ||||
-rw-r--r-- | vernac/indschemes.mli | 7 | ||||
-rw-r--r-- | vernac/lemmas.ml | 6 | ||||
-rw-r--r-- | vernac/metasyntax.ml | 22 | ||||
-rw-r--r-- | vernac/metasyntax.mli | 1 | ||||
-rw-r--r-- | vernac/obligations.ml | 6 | ||||
-rw-r--r-- | vernac/obligations.mli | 4 | ||||
-rw-r--r-- | vernac/proof_using.ml | 2 | ||||
-rw-r--r-- | vernac/record.ml | 17 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 63 | ||||
-rw-r--r-- | vernac/vernacprop.ml | 12 |
18 files changed, 106 insertions, 104 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 bcffe640c..f63206216 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -89,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 @@ -789,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; } @@ -847,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 @@ -1101,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 *) @@ -1400,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; @@ -1408,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 -> @@ -1421,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 *) @@ -1448,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 *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 9137f7a7e..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 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/vernacentries.ml b/vernac/vernacentries.ml index fa457c895..689d7a423 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 @@ -471,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" @@ -491,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 @@ -546,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)) @@ -582,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") @@ -637,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 = @@ -660,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 @@ -678,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 @@ -689,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 @@ -719,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."); @@ -735,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 = @@ -765,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") @@ -778,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 @@ -975,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 @@ -1211,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 @@ -1824,7 +1825,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 @@ -2015,7 +2016,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 *) @@ -2233,12 +2234,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 |