diff options
59 files changed, 358 insertions, 377 deletions
diff --git a/dev/base_include b/dev/base_include index 3320a2a94..1fb80dc07 100644 --- a/dev/base_include +++ b/dev/base_include @@ -230,7 +230,7 @@ let pf_e gl s = let _ = Flags.in_debugger := false let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference - (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));; + (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));; let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc) diff --git a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh new file mode 100644 index 000000000..a785290e7 --- /dev/null +++ b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "6837" ] || [ "$CI_BRANCH" = "located+libnames" ]; then + + ltac2_CI_BRANCH=located+libnames + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=located+libnames + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + Elpi_CI_BRANCH=located+libnames + Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git + + coq_dpdgraph_CI_BRANCH=located+libnames + coq_dpdgraph_CI_GITURL=https://github.com/ejgallego/coq-dpdgraph.git + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 74cdd788b..ba0c54407 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -547,7 +547,7 @@ let encode_path ?loc prefix mpdir suffix id = | Some (mp,dir) -> (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@ DirPath.repr dir) in - Qualid (Loc.tag ?loc @@ make_qualid + CAst.make ?loc @@ Qualid (make_qualid (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id) let raw_string_of_ref ?loc _ = function @@ -567,9 +567,9 @@ let raw_string_of_ref ?loc _ = function encode_path ?loc "SECVAR" None [] id let short_string_of_ref ?loc _ = function - | VarRef id -> Ident (Loc.tag ?loc id) - | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (Constant.repr3 cst))) - | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (MutInd.repr3 kn))) + | VarRef id -> CAst.make ?loc @@ Ident id + | ConstRef cst -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (Constant.repr3 cst))) + | IndRef (kn,0) -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (MutInd.repr3 kn))) | IndRef (kn,i) -> encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))] (Id.of_string ("_"^string_of_int i)) diff --git a/engine/uState.ml b/engine/uState.ml index 1dd8acd0d..6c8dbe3f4 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -296,7 +296,7 @@ let constrain_variables diff ctx = let reference_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try Libnames.Ident (Loc.tag @@ Option.get (Univ.LMap.find l map_rev).uname) + try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> Universes.reference_of_level l diff --git a/engine/universes.ml b/engine/universes.ml index ddc9beff4..e5f9212a7 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -21,7 +21,7 @@ open Nametab module UPairs = OrderedType.UnorderedPair(Univ.Level) module UPairSet = Set.Make (UPairs) -let reference_of_level l = +let reference_of_level l = CAst.make @@ match Level.name l with | Some (d, n as na) -> let qid = @@ -29,8 +29,8 @@ let reference_of_level l = with Not_found -> let name = Id.of_string_soft (string_of_int n) in Libnames.make_qualid d name - in Libnames.Qualid (Loc.tag @@ qid) - | None -> Libnames.Ident (Loc.tag @@ Id.of_string_soft (Level.to_string l)) + in Libnames.Qualid qid + | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l)) let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 541da3b6d..6b7efc839 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -289,7 +289,7 @@ let pattern_of_string ?env s = let dirpath_of_string_list s = let path = String.concat "." s in let m = Pcoq.parse_string Pcoq.Constr.global path in - let (_, qid) = Libnames.qualid_of_reference m in + let {CAst.v=qid} = Libnames.qualid_of_reference m in let id = try Nametab.full_name_module qid with Not_found -> diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 8bf530e7f..4ee13c961 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -10,6 +10,7 @@ open Pp open Util +open CAst open Names open Nameops open Libnames @@ -278,7 +279,7 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with List.fold_left (cases_pattern_fold_names f) (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat - | CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a + | CPatAtom (Some {v=Ident id}) when not (is_constructor id) -> f id a | CPatPrim _ | CPatAtom _ -> a | CPatCast ({CAst.loc},_) -> CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names" @@ -361,7 +362,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function let free_vars_of_constr_expr c = let rec aux bdvars l = function - | { CAst.v = CRef (Ident (_,id),_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l + | { CAst.v = CRef ({v=Ident id},_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c in aux [] Id.Set.empty c @@ -439,8 +440,8 @@ let map_constr_expr_with_binders g f e = CAst.map (function (* Used in constrintern *) let rec replace_vars_constr_expr l = function - | { CAst.loc; v = CRef (Ident (loc_id,id),us) } as x -> - (try CAst.make ?loc @@ CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x) + | { CAst.loc; v = CRef ({v=Ident id},us) } as x -> + (try CAst.make ?loc @@ CRef (make ?loc @@ Ident (Id.Map.find id l),us) with Not_found -> x) | c -> map_constr_expr_with_binders Id.Map.remove replace_vars_constr_expr l c @@ -511,7 +512,7 @@ let split_at_annot bl na = (** Pseudo-constructors *) -let mkIdentC id = CAst.make @@ CRef (Ident (Loc.tag id),None) +let mkIdentC id = CAst.make @@ CRef (make @@ Ident id,None) let mkRefC r = CAst.make @@ CRef (r,None) let mkCastC (a,k) = CAst.make @@ CCast (a,k) let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b) @@ -530,21 +531,21 @@ let mkCProdN ?loc bll c = let mkCLambdaN ?loc bll c = CAst.make ?loc @@ CLambdaN (bll,c) -let coerce_reference_to_id = function - | Ident (_,id) -> id - | Qualid (loc,_) -> +let coerce_reference_to_id = CAst.with_loc_val (fun ?loc -> function + | Ident id -> id + | Qualid _ -> CErrors.user_err ?loc ~hdr:"coerce_reference_to_id" - (str "This expression should be a simple identifier.") + (str "This expression should be a simple identifier.")) let coerce_to_id = function - | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?loc id + | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc id | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_id" (str "This expression should be a simple identifier.") let coerce_to_name = function - | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?loc @@ Name id - | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous + | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id + | { CAst.loc; v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") @@ -570,7 +571,7 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function CPatAtom (Some r) | CHole (None,Misctypes.IntroAnonymous,None) -> CPatAtom None - | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' -> + | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' -> CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id)) | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args -> (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f5a6a082e..19444988b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -215,7 +215,7 @@ let is_record indsp = let encode_record r = let indsp = global_inductive r in if not (is_record indsp) then - user_err ?loc:(loc_of_reference r) ~hdr:"encode_record" + user_err ?loc:r.CAst.loc ~hdr:"encode_record" (str "This type is not a structure type."); indsp @@ -271,14 +271,14 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - Qualid (Loc.tag ?loc @@ shortest_qualid_of_global vars r) + make @@ Qualid (shortest_qualid_of_global vars r) let my_extern_reference = ref default_extern_reference let set_extern_reference f = my_extern_reference := f let get_extern_reference () = !my_extern_reference -let extern_reference ?loc vars l = !my_extern_reference ?loc vars l +let extern_reference ?loc vars l = !my_extern_reference vars l (**********************************************************************) (* mapping patterns to cases_pattern_expr *) @@ -389,7 +389,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = (uninterp_cases_pattern_notations pat) with No_match -> lift (fun ?loc -> function - | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) + | PatVar (Name id) -> CPatAtom (Some (make ?loc @@ Ident id)) | PatVar (Anonymous) -> CPatAtom None | PatCstr(cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes vars) args in @@ -407,7 +407,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = (* we don't want to have 'x := _' in our patterns *) acc | Some c, _ -> - ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc) + ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc) | _ -> raise No_match in ip q tail acc | _ -> assert false @@ -415,7 +415,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = CPatRecord(List.rev (ip projs args [])) with Not_found | No_match | Exit -> - let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in + let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in if !asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) @@ -458,7 +458,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key end | SynDefRule kn -> - let qid = Qualid (Loc.tag ?loc @@ shortest_qualid_of_syndef vars kn) in + let qid = make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn) in let l1 = List.rev_map (fun (c,(scopt,scl)) -> extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) @@ -484,7 +484,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None - | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (Ident (loc,id))) + | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (make ?loc @@ Ident id)) with No_match -> extern_notation_pattern allscopes vars t rules @@ -745,9 +745,9 @@ let rec extern inctx scopes vars r = with No_match -> lift (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) - (extern_reference ?loc vars ref) (extern_universes us) + (extern_reference vars ref) (extern_universes us) - | GVar id -> CRef (Ident (loc,id),None) + | GVar id -> CRef (make ?loc @@ Ident id,None) | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None) @@ -763,7 +763,6 @@ let rec extern inctx scopes vars r = | GApp (f,args) -> (match DAst.get f with | GRef (ref,us) -> - let rloc = f.CAst.loc in let subscopes = find_arguments_scope ref in let args = fill_arg_scopes args subscopes (snd scopes) in begin @@ -802,7 +801,7 @@ let rec extern inctx scopes vars r = (* we give up since the constructor is not complete *) | (arg, scopes) :: tail -> let head = extern true scopes vars arg in - ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) + ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) in CRecord (List.rev (ip projs locals args [])) with @@ -810,7 +809,7 @@ let rec extern inctx scopes vars r = let args = extern_args (extern true) vars args in extern_app inctx (select_stronger_impargs (implicits_of_global ref)) - (Some ref,extern_reference ?loc:rloc vars ref) (extern_universes us) args + (Some ref,extern_reference ?loc vars ref) (extern_universes us) args end | _ -> @@ -1090,7 +1089,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function List.map (fun (c,(scopt,scl)) -> extern true (scopt,scl@scopes) vars c, None) terms in - let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in + let a = CRef (make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn),None) in CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in if List.is_empty args then e else diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 55b943eac..f2cd07c94 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -96,7 +96,7 @@ let is_global id = false let global_reference_of_reference ref = - locate_reference (snd (qualid_of_reference ref)) + locate_reference (qualid_of_reference ref).CAst.v let global_reference id = locate_reference (qualid_of_ident id) @@ -403,7 +403,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars let name = let id = match ty with - | { CAst.v = CApp ((_, { CAst.v = CRef (Ident (loc,id),_) } ), _) } -> id + | { v = CApp ((_, { v = CRef ({v=Ident id},_) } ), _) } -> id | _ -> default_non_dependent_ident in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name @@ -554,8 +554,8 @@ let is_var store pat = | _ -> false let out_var pat = - match pat.CAst.v with - | CPatAtom (Some (Ident (_,id))) -> Name id + match pat.v with + | CPatAtom (Some ({v=Ident id})) -> Name id | CPatAtom None -> Anonymous | _ -> assert false @@ -621,18 +621,18 @@ let error_cannot_coerce_disjunctive_pattern_term ?loc () = let terms_of_binders bl = let rec term_of_pat pt = dmap_with_loc (fun ?loc -> function - | PatVar (Name id) -> CRef (Ident (loc,id), None) + | PatVar (Name id) -> CRef (make @@ Ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in + let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with | bnd :: l -> - let loc = bnd.CAst.loc in + let loc = bnd.loc in begin match DAst.get bnd with - | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l + | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (make ?loc @@ Ident id, None)) :: extract_variables l | GLocalDef (Name id,_,_,_) -> extract_variables l | GLocalDef (Anonymous,_,_,_) | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.") @@ -720,7 +720,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in match disjpat with | [pat] -> (glob_constr_of_cases_pattern pat, None) - | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc () + | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in let terms = Id.Map.map mk_env terms in let binders = Id.Map.map mk_env' binders in @@ -805,7 +805,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = distinction *) let cases_pattern_of_name {loc;v=na} = - let atom = match na with Name id -> Some (Ident (loc,id)) | Anonymous -> None in + let atom = match na with Name id -> Some (make ?loc @@ Ident id) | Anonymous -> None in CAst.make ?loc (CPatAtom atom) let split_by_type ids subst = @@ -902,7 +902,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = try let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in let expl_impls = List.map - (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (make ?loc @@ ExplByName id)) expl_impls in + (fun id -> CAst.make ?loc @@ CRef (make ?loc @@ Ident id,None), Some (make ?loc @@ ExplByName id)) expl_impls in let tys = string_of_ty ty in Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys; gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls @@ -969,14 +969,14 @@ let dump_extended_global loc = function | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref | SynDef sp -> Dumpglob.add_glob_kn ?loc sp -let intern_extended_global_of_qualid (loc,qid) = +let intern_extended_global_of_qualid {loc;v=qid} = let r = Nametab.locate_extended qid in dump_extended_global loc r; r let intern_reference ref = let qid = qualid_of_reference ref in let r = try intern_extended_global_of_qualid qid - with Not_found -> error_global_not_found ?loc:(fst qid) (snd qid) + with Not_found -> error_global_not_found qid in Smartlocate.global_of_extended_global r @@ -993,8 +993,9 @@ let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort = | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info] (* Is it a global reference or a syntactic definition? *) -let intern_qualid loc qid intern env ntnvars us args = - match intern_extended_global_of_qualid (loc,qid) with +let intern_qualid qid intern env ntnvars us args = + let loc = qid.loc in + match intern_extended_global_of_qualid qid with | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> let (ids,c) = Syntax_def.search_syntactic_definition sp in @@ -1007,9 +1008,9 @@ let intern_qualid loc qid intern env ntnvars us args = let infos = (Id.Map.empty, env) in let projapp = match c with NRef _ -> true | _ -> false in let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in - let loc = c.CAst.loc in + let loc = c.loc in let err () = - user_err ?loc (str "Notation " ++ pr_qualid qid + user_err ?loc (str "Notation " ++ pr_qualid qid.v ++ str " cannot have a universe instance," ++ str " its expanded head does not start with a reference") in @@ -1026,40 +1027,41 @@ let intern_qualid loc qid intern env ntnvars us args = | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) - user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) + user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v) | Some _, _ -> err () in c, projapp, args2 (* Rule out section vars since these should have been found by intern_var *) -let intern_non_secvar_qualid loc qid intern env ntnvars us args = - let c, _, _ as r = intern_qualid loc qid intern env ntnvars us args in +let intern_non_secvar_qualid qid intern env ntnvars us args = + let c, _, _ as r = intern_qualid qid intern env ntnvars us args in match DAst.get c with | GRef (VarRef _, _) -> raise Not_found | _ -> r let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function - | Qualid (loc, qid) -> + | {loc; v=Qualid qid} -> + let qid = make ?loc qid in let r,projapp,args2 = - try intern_qualid loc qid intern env ntnvars us args - with Not_found -> error_global_not_found ?loc qid + try intern_qualid qid intern env ntnvars us args + with Not_found -> error_global_not_found qid in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 - | Ident (loc, id) -> + | {loc; v=Ident id} -> try intern_var env lvar namedctx loc id us, args with Not_found -> - let qid = qualid_of_ident id in + let qid = make ?loc @@ qualid_of_ident id in try - let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env ntnvars us args in + let r, projapp, args2 = intern_non_secvar_qualid qid intern env ntnvars us args in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 with Not_found -> (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (gvar (loc,id) us, [], [], []), args - else error_global_not_found ?loc qid + else error_global_not_found qid let interp_reference vars r = let (r,_,_,_),_ = @@ -1255,8 +1257,8 @@ let find_constructor loc add_params ref = | None -> [] let find_pattern_variable = function - | Ident (loc,id) -> id - | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x)) + | {v=Ident id} -> id + | {loc;v=Qualid _} as x -> raise (InternalizationError(loc,NotAConstructor x)) let check_duplicate loc fields = let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in @@ -1289,7 +1291,7 @@ let sort_fields ~complete loc fields completer = let gr = global_reference_of_reference first_field_ref in (gr, Recordops.find_projection gr) with Not_found -> - user_err ?loc:(loc_of_reference first_field_ref) ~hdr:"intern" + user_err ?loc ~hdr:"intern" (pr_reference first_field_ref ++ str": Not a projection") in (* the number of parameters *) @@ -1297,7 +1299,7 @@ let sort_fields ~complete loc fields completer = (* the reference constructor of the record *) let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in - try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) + try make ?loc @@ Qualid (shortest_qualid_of_global Id.Set.empty global_record_id) with Not_found -> anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in @@ -1347,7 +1349,7 @@ let sort_fields ~complete loc fields completer = | (field_ref, field_value) :: fields -> let field_glob_ref = try global_reference_of_reference field_ref with Not_found -> - user_err ?loc:(loc_of_reference field_ref) ~hdr:"intern" + user_err ?loc ~hdr:"intern" (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in let remaining_projs, (field_index, _) = let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in @@ -1476,9 +1478,9 @@ let drop_notations_pattern looked_for genv = | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x in let rec drop_syndef top scopes re pats = - let (loc,qid) = qualid_of_reference re in + let qid = qualid_of_reference re in try - match locate_extended qid with + match locate_extended qid.v with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with @@ -1496,16 +1498,16 @@ let drop_notations_pattern looked_for genv = (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; let nvars = List.length vars in - if List.length pats < nvars then error_not_enough_arguments ?loc; + if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc; let pats1,pats2 = List.chop nvars pats in let subst = make_subst vars pats1 in - let idspl1 = List.map (in_not false loc scopes (subst, Id.Map.empty) []) args in + let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in let (_,argscs) = find_remaining_scopes pats1 pats2 g in Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2) | _ -> raise Not_found) | TrueGlobal g -> test_kind top g; - Dumpglob.add_glob ?loc g; + Dumpglob.add_glob ?loc:qid.loc g; let (_,argscs) = find_remaining_scopes [] pats g in Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats) with Not_found -> None @@ -1535,7 +1537,7 @@ let drop_notations_pattern looked_for genv = | None -> raise (InternalizationError (loc,NotAConstructor head)) end | CPatCstr (r, Some expl_pl, pl) -> - let g = try locate (snd (qualid_of_reference r)) + let g = try locate (qualid_of_reference r).v with Not_found -> raise (InternalizationError (loc,NotAConstructor r)) in if expl_pl == [] then diff --git a/interp/declare.ml b/interp/declare.ml index 7dd73fbb5..c55a6c69b 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -592,15 +592,10 @@ let input_constraints : constraint_decl -> Libobject.obj = discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } -let loc_of_glob_level = function - | Misctypes.GType (Misctypes.UNamed n) -> Libnames.loc_of_reference n - | _ -> None - let do_constraint poly l = let u_of_id x = let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - let loc = loc_of_glob_level x in - loc, Universes.is_polymorphic level, level + Universes.is_polymorphic level, level in let in_section = Lib.sections_are_opened () in let () = @@ -608,18 +603,17 @@ let do_constraint poly l = user_err ~hdr:"Constraint" (str"Cannot declare polymorphic constraints outside sections") in - let check_poly ?loc p loc' p' = + let check_poly p p' = if poly then () else if p || p' then - let loc = if p then loc else loc' in - user_err ?loc ~hdr:"Constraint" + user_err ~hdr:"Constraint" (str "Cannot declare a global constraint on " ++ str "a polymorphic universe, use " ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let ploc, p, lu = u_of_id l and rloc, p', ru = u_of_id r in - check_poly ?loc:ploc p rloc p'; + let p, lu = u_of_id l and p', ru = u_of_id r in + check_poly p p'; Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 7d919ec0c..a1a3be70f 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -94,8 +94,8 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = else l in let rec aux bdvars l c = match CAst.(c.v) with - | CRef (Ident (loc,id),_) -> found loc id bdvars l - | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) -> + | CRef ({CAst.v=Ident id},_) -> found c.CAst.loc id bdvars l + | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef ({CAst.v=Ident id},_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c @@ -194,7 +194,7 @@ let combine_params avoid fn applied needed = let combine_params_freevar = fun avoid (_, decl) -> let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (CAst.make @@ CRef (Ident (Loc.tag id'),None), Id.Set.add id' avoid) + (CAst.make @@ CRef (CAst.make @@ Ident id',None), Id.Set.add id' avoid) let destClassApp cl = let open CAst in @@ -202,7 +202,7 @@ let destClassApp cl = match cl.v with | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst) | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst) - | CRef (ref, inst) -> CAst.make ?loc:(loc_of_reference ref) (ref, [], inst) + | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) | _ -> raise Not_found let destClassAppExpl cl = @@ -210,15 +210,15 @@ let destClassAppExpl cl = let loc = cl.loc in match cl.v with | CApp ((None, { v = CRef (ref, inst) } ), l) -> CAst.make ?loc (ref, l, inst) - | CRef (ref, inst) -> CAst.make ?loc:(loc_of_reference ref) (ref, [], inst) + | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) | _ -> raise Not_found let implicit_application env ?(allow_partial=true) f ty = let is_class = try let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in - let (loc, qid) = qualid_of_reference r in - let gr = Nametab.locate qid in + let qid = qualid_of_reference r in + let gr = Nametab.locate qid.CAst.v in if Typeclasses.is_class gr then Some (clapp, gr) else None with Not_found -> None in diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 6033d509b..1f4a93a6f 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -42,42 +42,38 @@ let global_of_extended_global = function | [],NApp (NRef ref,[]) -> ref | _ -> raise Not_found -let locate_global_with_alias ?(head=false) (loc,qid) = +let locate_global_with_alias ?(head=false) {CAst.loc; v=qid} = let ref = Nametab.locate_extended qid in try if head then global_of_extended_global_head ref else global_of_extended_global ref with Not_found -> - user_err ?loc (pr_qualid qid ++ + user_err ?loc (pr_qualid qid ++ str " is bound to a notation that does not denote a reference.") -let global_inductive_with_alias r = - let (loc,qid as lqid) = qualid_of_reference r in - try match locate_global_with_alias lqid with +let global_inductive_with_alias ({CAst.loc} as lr) = + let qid = qualid_of_reference lr in + try match locate_global_with_alias qid with | IndRef ind -> ind | ref -> - user_err ?loc:(loc_of_reference r) ~hdr:"global_inductive" - (pr_reference r ++ spc () ++ str "is not an inductive type.") - with Not_found -> Nametab.error_global_not_found ?loc qid + user_err ?loc ~hdr:"global_inductive" + (pr_reference lr ++ spc () ++ str "is not an inductive type.") + with Not_found -> Nametab.error_global_not_found qid let global_with_alias ?head r = - let (loc,qid as lqid) = qualid_of_reference r in - try locate_global_with_alias ?head lqid - with Not_found -> Nametab.error_global_not_found ?loc qid + let qid = qualid_of_reference r in + try locate_global_with_alias ?head qid + with Not_found -> Nametab.error_global_not_found qid -let smart_global ?head = function +let smart_global ?head = CAst.with_loc_val (fun ?loc -> function | AN r -> - global_with_alias ?head r - | ByNotation {CAst.loc;v=(ntn,sc)} -> - Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc + global_with_alias ?head r + | ByNotation (ntn,sc) -> + Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc) -let smart_global_inductive = function +let smart_global_inductive = CAst.with_loc_val (fun ?loc -> function | AN r -> - global_inductive_with_alias r - | ByNotation {CAst.loc;v=(ntn,sc)} -> - destIndRef - (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc) - -let loc_of_smart_reference = function - | AN r -> loc_of_reference r - | ByNotation {CAst.loc;v=(_,_)} -> loc + global_inductive_with_alias r + | ByNotation (ntn,sc) -> + destIndRef + (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc)) diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 112301251..7ff7e899e 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Loc open Names open Libnames open Globnames @@ -19,7 +18,7 @@ open Misctypes if not bound in the global env; raise a [UserError] if bound to a syntactic def that does not denote a reference *) -val locate_global_with_alias : ?head:bool -> qualid located -> global_reference +val locate_global_with_alias : ?head:bool -> qualid CAst.t -> global_reference (** Extract a global_reference from a reference that can be an "alias" *) val global_of_extended_global : extended_global_reference -> global_reference @@ -38,6 +37,3 @@ val smart_global : ?head:bool -> reference or_by_notation -> global_reference (** The same for inductive types *) val smart_global_inductive : reference or_by_notation -> inductive - -(** Return the loc of a smart reference *) -val loc_of_smart_reference : reference or_by_notation -> Loc.t option diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 0958cc7ee..e5ed58be6 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Misctypes open Genarg open Geninterp @@ -32,10 +31,6 @@ let wit_string : string uniform_genarg_type = let wit_pre_ident : string uniform_genarg_type = make0 "preident" -let loc_of_or_by_notation f = function - | AN c -> f c - | ByNotation {CAst.loc;v=(s,_)} -> loc - let wit_int_or_var = make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var" diff --git a/interp/stdarg.mli b/interp/stdarg.mli index b69129956..53d1a522d 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -22,9 +22,6 @@ open Misctypes open Tactypes open Genarg -(** FIXME: nothing to do there. *) -val loc_of_or_by_notation : ('a -> Loc.t option) -> 'a or_by_notation -> Loc.t option - val wit_unit : unit uniform_genarg_type val wit_bool : bool uniform_genarg_type diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 1eee3dfc7..9eb6f62cc 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -113,9 +113,11 @@ type 'a or_var = type 'a and_short_name = 'a * lident option -type 'a or_by_notation = +type 'a or_by_notation_r = | AN of 'a - | ByNotation of (string * string option) CAst.t + | ByNotation of (string * string option) + +type 'a or_by_notation = 'a or_by_notation_r CAst.t (* NB: the last string in [ByNotation] is actually a [Notation.delimiters], but this formulation avoids a useless dependency. *) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index dca491057..df061bfb7 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -106,7 +106,7 @@ type comment = | CommentString of string | CommentInt of int -type reference_or_constr = +type reference_or_constr = | HintsReference of reference | HintsConstr of constr_expr diff --git a/library/libnames.ml b/library/libnames.ml index 81af5f2c9..d84731322 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -190,54 +190,51 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with | DirClosedSection dp1, DirClosedSection dp2 -> DirPath.equal dp1 dp2 | _ -> false -type reference = - | Qualid of qualid Loc.located - | Ident of Id.t Loc.located - -let qualid_of_reference = function - | Qualid (loc,qid) -> loc, qid - | Ident (loc,id) -> loc, qualid_of_ident id - -let string_of_reference = function - | Qualid (loc,qid) -> string_of_qualid qid - | Ident (loc,id) -> Id.to_string id - -let pr_reference = function - | Qualid (_,qid) -> pr_qualid qid - | Ident (_,id) -> Id.print id - -let loc_of_reference = function - | Qualid (loc,qid) -> loc - | Ident (loc,id) -> loc - -let eq_reference r1 r2 = match r1, r2 with -| Qualid (_, q1), Qualid (_, q2) -> qualid_eq q1 q2 -| Ident (_, id1), Ident (_, id2) -> Id.equal id1 id2 +type reference_r = + | Qualid of qualid + | Ident of Id.t +type reference = reference_r CAst.t + +let qualid_of_reference = CAst.map (function + | Qualid qid -> qid + | Ident id -> qualid_of_ident id) + +let string_of_reference = CAst.with_val (function + | Qualid qid -> string_of_qualid qid + | Ident id -> Id.to_string id) + +let pr_reference = CAst.with_val (function + | Qualid qid -> pr_qualid qid + | Ident id -> Id.print id) + +let eq_reference {CAst.v=r1} {CAst.v=r2} = match r1, r2 with +| Qualid q1, Qualid q2 -> qualid_eq q1 q2 +| Ident id1, Ident id2 -> Id.equal id1 id2 | _ -> false -let join_reference ns r = +let join_reference {CAst.loc=l1;v=ns} {CAst.loc=l2;v=r} = + CAst.make ?loc:(Loc.merge_opt l1 l2) ( match ns , r with - Qualid (_, q1), Qualid (loc, q2) -> + Qualid q1, Qualid q2 -> let (dp1,id1) = repr_qualid q1 in let (dp2,id2) = repr_qualid q2 in - Qualid (loc, - make_qualid + Qualid (make_qualid (append_dirpath (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) dp2) id2) - | Qualid (_, q1), Ident (loc, id2) -> + | Qualid q1, Ident id2 -> let (dp1,id1) = repr_qualid q1 in - Qualid (loc, - make_qualid + Qualid (make_qualid (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) id2) - | Ident (_, id1), Qualid (loc, q2) -> + | Ident id1, Qualid q2 -> let (dp2,id2) = repr_qualid q2 in - Qualid (loc, make_qualid + Qualid (make_qualid (append_dirpath (dirpath_of_string (Names.Id.to_string id1)) dp2) id2) - | Ident (_, id1), Ident (loc, id2) -> - Qualid (loc, make_qualid + | Ident id1, Ident id2 -> + Qualid (make_qualid (dirpath_of_string (Names.Id.to_string id1)) id2) + ) (* Default paths *) let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/libnames.mli b/library/libnames.mli index afceef530..9dad26129 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -9,7 +9,6 @@ (************************************************************************) open Util -open Loc open Names (** {6 Dirpaths } *) @@ -137,15 +136,15 @@ val eq_global_dir_reference : global name (referred either by a qualified name or by a single name) or a variable *) -type reference = - | Qualid of qualid located - | Ident of Id.t located +type reference_r = + | Qualid of qualid + | Ident of Id.t +type reference = reference_r CAst.t val eq_reference : reference -> reference -> bool -val qualid_of_reference : reference -> qualid located +val qualid_of_reference : reference -> qualid CAst.t val string_of_reference : reference -> string val pr_reference : reference -> Pp.t -val loc_of_reference : reference -> Loc.t option val join_reference : reference -> reference -> reference (** some preset paths *) diff --git a/library/library.ml b/library/library.ml index fb9b54462..56d2709d5 100644 --- a/library/library.ml +++ b/library/library.ml @@ -577,7 +577,7 @@ let require_library_from_dirpath modrefl export = (* the function called by Vernacentries.vernac_import *) -let safe_locate_module (loc,qid) = +let safe_locate_module {CAst.loc;v=qid} = try Nametab.locate_module qid with Not_found -> user_err ?loc ~hdr:"import_library" @@ -595,7 +595,7 @@ let import_module export modl = | [] -> () | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in let rec aux acc = function - | (loc, dir as m) :: l -> + | ({CAst.loc; v=dir} as m) :: l -> let m,acc = try Nametab.locate_module dir, acc with Not_found-> flush acc; safe_locate_module m, [] in diff --git a/library/library.mli b/library/library.mli index 82a891acc..0877ebb5a 100644 --- a/library/library.mli +++ b/library/library.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Loc open Names open Libnames @@ -37,7 +36,7 @@ type seg_proofs = Constr.constr Future.computation array (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) -val import_module : bool -> qualid located list -> unit +val import_module : bool -> qualid CAst.t list -> unit (** Start the compilation of a file as a library. The first argument must be output file, and the diff --git a/library/nametab.ml b/library/nametab.ml index 0e996443f..2046bf758 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -18,8 +18,8 @@ open Globnames exception GlobalizationError of qualid -let error_global_not_found ?loc q = - Loc.raise ?loc (GlobalizationError q) +let error_global_not_found {CAst.loc;v} = + Loc.raise ?loc (GlobalizationError v) (* The visibility can be registered either - for all suffixes not shorter then a given int - when the object @@ -459,16 +459,16 @@ let global_of_path sp = let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab -let global r = - let (loc,qid) = qualid_of_reference r in - try match locate_extended qid with +let global ({CAst.loc;v=r} as lr)= + let {CAst.loc; v} as qid = qualid_of_reference lr in + try match locate_extended v with | TrueGlobal ref -> ref | SynDef _ -> user_err ?loc ~hdr:"global" (str "Unexpected reference to a notation: " ++ - pr_qualid qid) + pr_qualid v) with Not_found -> - error_global_not_found ?loc qid + error_global_not_found qid (* Exists functions ********************************************************) @@ -539,13 +539,12 @@ let pr_global_env env ref = with Not_found as e -> if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e -let global_inductive r = - match global r with +let global_inductive ({CAst.loc; v=r} as lr) = + match global lr with | IndRef ind -> ind | ref -> - user_err ?loc:(loc_of_reference r) ~hdr:"global_inductive" - (pr_reference r ++ spc () ++ str "is not an inductive type") - + user_err ?loc ~hdr:"global_inductive" + (pr_reference lr ++ spc () ++ str "is not an inductive type") (********************************************************************) diff --git a/library/nametab.mli b/library/nametab.mli index 3802eaa9a..cd28518ab 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -61,7 +61,7 @@ open Globnames exception GlobalizationError of qualid (** Raises a globalization error *) -val error_global_not_found : ?loc:Loc.t -> qualid -> 'a +val error_global_not_found : qualid CAst.t -> 'a (** {6 Register visibility of things } *) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index c0ead3a0a..5f63d21c4 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -312,7 +312,7 @@ let interp_entry forpat e = match e with let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with | Anonymous -> CPatAtom None - | Name id -> CPatAtom (Some (Ident (Loc.tag ?loc id))) + | Name id -> CPatAtom (Some (CAst.make ?loc @@ Ident id)) type 'r env = { constrs : 'r list; diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index b4f09ee6a..9c2806bea 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -200,11 +200,11 @@ GEXTEND Gram | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args) | "@"; lid = pattern_identref; args=LIST1 identref -> let { CAst.loc = locid; v = id } = lid in - let args = List.map (fun x -> CAst.make @@ CRef (Ident Loc.(tag ?loc:x.CAst.loc x.CAst.v), None), None) args in + let args = List.map (fun x -> CAst.make @@ CRef (CAst.make ?loc:x.CAst.loc @@ Ident x.CAst.v, None), None) args in CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> - CAst.make ~loc:!@loc @@ CAppExpl ((None, Ident (Loc.tag ~loc:!@loc ldots_var),None),[c]) ] + CAst.make ~loc:!@loc @@ CAppExpl ((None, CAst.make ~loc:!@loc @@ Ident ldots_var, None),[c]) ] | "8" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 69dc391c4..b25ea766a 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -77,16 +77,16 @@ GEXTEND Gram ; reference: [ [ id = ident; (l,id') = fields -> - Qualid (Loc.tag ~loc:!@loc @@ local_make_qualid (l@[id]) id') - | id = ident -> Ident (Loc.tag ~loc:!@loc id) + CAst.make ~loc:!@loc @@ Qualid (local_make_qualid (l@[id]) id') + | id = ident -> CAst.make ~loc:!@loc @@ Ident id ] ] ; by_notation: - [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> CAst.make ~loc:!@loc (s, sc) ] ] + [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (s, sc) ] ] ; smart_global: - [ [ c = reference -> Misctypes.AN c - | ntn = by_notation -> Misctypes.ByNotation ntn ] ] + [ [ c = reference -> CAst.make ~loc:!@loc @@ Misctypes.AN c + | ntn = by_notation -> CAst.make ~loc:!@loc @@ Misctypes.ByNotation ntn ] ] ; qualid: [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ] diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 99eec9742..72c3cc14a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -624,9 +624,9 @@ GEXTEND Gram VernacSetStrategy l (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> - VernacCanonical (AN qid) + VernacCanonical CAst.(make ~loc:!@loc @@ AN qid) | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> - VernacCanonical (ByNotation ntn) + VernacCanonical CAst.(make ~loc:!@loc @@ ByNotation ntn) | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d) @@ -640,10 +640,10 @@ GEXTEND Gram VernacIdentityCoercion (f, s, t) | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (AN qid, s, t) + VernacCoercion (CAst.make ~loc:!@loc @@ AN qid, s, t) | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (ByNotation ntn, s, t) + VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t) | IDENT "Context"; c = binders -> VernacContext c diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 0f8aad110..9f186224b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -210,7 +210,7 @@ module Prim : val qualid : qualid CAst.t Gram.entry val fullyqualid : Id.t list CAst.t Gram.entry val reference : reference Gram.entry - val by_notation : (string * string option) CAst.t Gram.entry + val by_notation : (string * string option) Gram.entry val smart_global : reference or_by_notation Gram.entry val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index a4e8c44cd..397cb2920 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -597,8 +597,8 @@ let warns () = let rec locate_ref = function | [] -> [],[] | r::l -> - let q = snd (qualid_of_reference r) in - let mpo = try Some (Nametab.locate_module q) with Not_found -> None + let q = qualid_of_reference r in + let mpo = try Some (Nametab.locate_module q.CAst.v) with Not_found -> None and ro = try Some (Smartlocate.global_with_alias r) with Nametab.GlobalizationError _ | UserError _ -> None @@ -608,7 +608,7 @@ let rec locate_ref = function | None, Some r -> let refs,mps = locate_ref l in r::refs,mps | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps | Some mp, Some r -> - warning_ambiguous_name (q,mp,r); + warning_ambiguous_name (q.CAst.v,mp,r); let refs,mps = locate_ref l in refs,mp::mps (*s Recursive extraction in the Coq toplevel. The vernacular command is @@ -646,7 +646,7 @@ let separate_extraction lr = is \verb!Extraction! [qualid]. *) let simple_extraction r = - Vernacentries.dump_global (Misctypes.AN r); + Vernacentries.dump_global CAst.(make (Misctypes.AN r)); match locate_ref [r] with | ([], [mp]) as p -> full_extr None p | [r],[] -> diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 6c421491f..54c6d9d72 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -899,7 +899,7 @@ let extract_constant_inline inline r ids s = let extract_inductive r s l optstr = check_inside_section (); let g = Smartlocate.global_with_alias r in - Dumpglob.add_glob ?loc:(loc_of_reference r) g; + Dumpglob.add_glob ?loc:r.CAst.loc g; match g with | IndRef ((kn,i) as ip) -> let mib = Global.lookup_mind kn in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 1c27b27e2..b65d9867d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -356,7 +356,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (*i The next call to mk_rel_id is valid since we have just construct the graph Ensures by : do_built i*) - let f_R_mut = Ident (Loc.tag @@ mk_rel_id (List.nth names 0)) in + let f_R_mut = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in let ind_kn = fst (locate_with_msg (pr_reference f_R_mut++str ": Not an inductive type!") @@ -364,7 +364,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error f_R_mut) in let fname_kn (((fname,_),_,_,_,_),_) = - let f_ref = Ident CAst.(with_loc_val (fun ?loc n -> (loc,n)) fname) in + let f_ref = CAst.map (fun n -> Ident n) fname in locate_with_msg (pr_reference f_ref++str ": Not an inductive type!") locate_constant @@ -472,7 +472,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( - (None,(Ident (Loc.tag fname)),None) , + (None,CAst.make @@ Ident fname,None) , (List.map (function | {CAst.v=Anonymous} -> assert false @@ -482,7 +482,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))), + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in @@ -539,7 +539,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> let ltof = let make_dir l = DirPath.make (List.rev_map Id.of_string l) in - Libnames.Qualid (Loc.tag @@ Libnames.qualid_of_path + CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) in let fun_from_mes = @@ -724,7 +724,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let rec add_args id new_args = CAst.map (function | CRef (r,_) as b -> begin match r with - | Libnames.Ident(loc,fname) when Id.equal fname id -> + | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> CAppExpl((None,r,None),new_args) | _ -> b end @@ -744,7 +744,7 @@ let rec add_args id new_args = CAst.map (function | CAppExpl((pf,r,us),exprl) -> begin match r with - | Libnames.Ident(loc,fname) when Id.equal fname id -> + | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl)) | _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl) end @@ -883,7 +883,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None)) + CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None)) nal | Constrexpr.CLocalPattern _ -> assert false ) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index d6fd2f2a0..a0b9217c7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -32,7 +32,7 @@ let id_of_name = function | _ -> raise Not_found let locate ref = - let (loc,qid) = qualid_of_reference ref in + let {CAst.v=qid} = qualid_of_reference ref in Nametab.locate qid let locate_ind ref = @@ -100,13 +100,8 @@ let list_union_eq eq_fun l1 l2 = let list_add_set_eq eq_fun x l = if List.exists (eq_fun x) l then l else x::l - - - let const_of_id id = - let _,princ_ref = - qualid_of_reference (Libnames.Ident (Loc.tag id)) - in + let princ_ref = qualid_of_ident id in try Constrintern.locate_reference princ_ref with Not_found -> CErrors.user_err ~hdr:"IndFun.const_of_id" diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 4cbcde8e5..fb9ae64bf 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1325,7 +1325,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = - let na_ref = Libnames.Ident (Loc.tag na) in + let na_ref = CAst.make @@ Libnames.Ident na in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1579,7 +1579,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.tag term_id)] in + let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ Ident term_id] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 1909cd96f..0c42a8bb2 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -38,11 +38,11 @@ let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac -let reference_to_id = function - | Libnames.Ident (loc, id) -> CAst.make ?loc id - | Libnames.Qualid (loc,_) -> +let reference_to_id = CAst.map_with_loc (fun ?loc -> function + | Libnames.Ident id -> id + | Libnames.Qualid _ -> CErrors.user_err ?loc - (str "This expression should be a simple identifier.") + (str "This expression should be a simple identifier.")) let tactic_mode = Gram.entry_create "vernac:tactic_command" @@ -473,7 +473,7 @@ END VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY | [ "Print" "Ltac" reference(r) ] -> - [ Feedback.msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ] + [ Feedback.msg_notice (Tacintern.print_ltac (Libnames.qualid_of_reference r).CAst.v) ] END VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY @@ -508,8 +508,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r - | TacticRedefinition (Ident (_,r),_) -> r - | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater + | TacticRedefinition ({CAst.v=Ident r},_) -> r + | TacticRedefinition ({CAst.v=Qualid q},_) -> snd(repr_qualid q)) l), VtLater ] -> [ fun ~atts ~st -> let open Vernacinterp in Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; st diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 54e2ba960..352e92c2a 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -49,7 +49,7 @@ module Tactic = Pltac open Pcoq -let sigref = mkRefC (Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Init.Specif.sig")) +let sigref = mkRefC (CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Init.Specif.sig")) type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 7643cc97d..7534e2799 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -154,8 +154,7 @@ let mkTacCase with_evar = function (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [(clear,ElimOnIdent id),(None,None),None],None -> - let id = CAst.(id.loc, id.v) in - TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings))) + TacCase (with_evar,(clear,(CAst.make @@ CRef (CAst.make ?loc:id.CAst.loc @@ Ident id.CAst.v,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index a42994652..5d262ffcb 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -181,9 +181,9 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_and_short_name pr (c,_) = pr c - let pr_or_by_notation f = function + let pr_or_by_notation f = CAst.with_val (function | AN v -> f v - | ByNotation {CAst.v=(s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc) let pr_located pr (loc,x) = pr x diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e0368153e..d32a2faef 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1773,12 +1773,11 @@ let rec strategy_of_ast = function (* By default the strategy for "rewrite_db" is top-down *) -let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l) +let mkappc s l = CAst.make @@ CAppExpl ((None,CAst.make @@ Libnames.Ident (Id.of_string s),None),l) let declare_an_instance n s args = (((CAst.make @@ Name n),None), Explicit, - CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None), - args)) + CAst.make @@ CAppExpl ((None, CAst.make @@ Qualid (qualid_of_string s),None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] @@ -1792,17 +1791,17 @@ let anew_instance global binders instance fields = let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance global binders instance - [(Ident (Loc.tag @@ Id.of_string "reflexivity"),lemma)] + [(CAst.make @@ Ident (Id.of_string "reflexivity"),lemma)] let declare_instance_sym global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric" in anew_instance global binders instance - [(Ident (Loc.tag @@ Id.of_string "symmetry"),lemma)] + [(CAst.make @@ Ident (Id.of_string "symmetry"),lemma)] let declare_instance_trans global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" in anew_instance global binders instance - [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)] + [(CAst.make @@ Ident (Id.of_string "transitivity"),lemma)] let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = init_setoid (); @@ -1826,16 +1825,16 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( anew_instance global binders instance - [(Ident (Loc.tag @@ Id.of_string "PreOrder_Reflexive"), lemma1); - (Ident (Loc.tag @@ Id.of_string "PreOrder_Transitive"),lemma3)]) + [(CAst.make @@ Ident (Id.of_string "PreOrder_Reflexive"), lemma1); + (CAst.make @@ Ident (Id.of_string "PreOrder_Transitive"),lemma3)]) | (None, Some lemma2, Some lemma3) -> let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( anew_instance global binders instance - [(Ident (Loc.tag @@ Id.of_string "PER_Symmetric"), lemma2); - (Ident (Loc.tag @@ Id.of_string "PER_Transitive"),lemma3)]) + [(CAst.make @@ Ident (Id.of_string "PER_Symmetric"), lemma2); + (CAst.make @@ Ident (Id.of_string "PER_Transitive"),lemma3)]) | (Some lemma1, Some lemma2, Some lemma3) -> let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in @@ -1843,9 +1842,9 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), lemma1); - (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), lemma2); - (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), lemma3)]) + [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), lemma1); + (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2); + (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)]) let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) @@ -1951,16 +1950,16 @@ let add_setoid global binders a aeq t n = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); - (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) + [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) let make_tactic name = let open Tacexpr in let tacpath = Libnames.qualid_of_string name in - let tacname = Qualid (Loc.tag tacpath) in - TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, []))) + let tacname = CAst.make @@ Qualid tacpath in + TacArg (Loc.tag @@ (TacCall (Loc.tag (tacname, [])))) let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> @@ -2010,7 +2009,7 @@ let add_morphism glob binders m s n = let instance = (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( - (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), + (None, CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 566fc2873..e510b9f59 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -450,11 +450,10 @@ let register_ltac local tacl = let () = if is_shadowed then warn_unusable_identifier id in NewTac id, body | Tacexpr.TacticRedefinition (ident, body) -> - let loc = loc_of_reference ident in let kn = - try Tacenv.locate_tactic (snd (qualid_of_reference ident)) + try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v with Not_found -> - CErrors.user_err ?loc + CErrors.user_err ?loc:ident.CAst.loc (str "There is no Ltac named " ++ pr_reference ident ++ str ".") in UpdateTac kn, body diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 45f4a45fc..9ad9e1520 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -92,15 +92,15 @@ let intern_int_or_var = intern_or_var (fun (n : int) -> n) let intern_string_or_var = intern_or_var (fun (s : string) -> s) let intern_global_reference ist = function - | Ident (loc,id) when find_var id ist -> + | {CAst.loc;v=Ident id} when find_var id ist -> ArgVar (make ?loc id) | r -> - let loc,_ as lqid = qualid_of_reference r in - try ArgArg (loc,locate_global_with_alias lqid) - with Not_found -> error_global_not_found (snd lqid) + let {CAst.loc} as lqid = qualid_of_reference r in + try ArgArg (loc,locate_global_with_alias lqid) + with Not_found -> error_global_not_found lqid let intern_ltac_variable ist = function - | Ident (loc,id) -> + | {loc;v=Ident id} -> if find_var id ist then (* A local variable of any type *) ArgVar (make ?loc id) @@ -109,19 +109,19 @@ let intern_ltac_variable ist = function raise Not_found let intern_constr_reference strict ist = function - | Ident (_,id) as r when not strict && find_hyp id ist -> + | {v=Ident id} as r when not strict && find_hyp id ist -> (DAst.make @@ GVar id), Some (make @@ CRef (r,None)) - | Ident (_,id) as r when find_var id ist -> + | {v=Ident id} as r when find_var id ist -> (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None)) | r -> - let loc,_ as lqid = qualid_of_reference r in + let {loc} as lqid = qualid_of_reference r in DAst.make @@ GRef (locate_global_with_alias lqid,None), if strict then None else Some (make @@ CRef (r,None)) (* Internalize an isolated reference in position of tactic *) let intern_isolated_global_tactic_reference r = - let (loc,qid) = qualid_of_reference r in + let {loc;v=qid} = qualid_of_reference r in TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) let intern_isolated_tactic_reference strict ist r = @@ -135,12 +135,12 @@ let intern_isolated_tactic_reference strict ist r = try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) with Not_found -> (* Reference not found *) - error_global_not_found (snd (qualid_of_reference r)) + error_global_not_found (qualid_of_reference r) (* Internalize an applied tactic reference *) let intern_applied_global_tactic_reference r = - let (loc,qid) = qualid_of_reference r in + let {loc;v=qid} = qualid_of_reference r in ArgArg (loc,Tacenv.locate_tactic qid) let intern_applied_tactic_reference ist r = @@ -151,7 +151,7 @@ let intern_applied_tactic_reference ist r = try intern_applied_global_tactic_reference r with Not_found -> (* Reference not found *) - error_global_not_found (snd (qualid_of_reference r)) + error_global_not_found (qualid_of_reference r) (* Intern a reference parsed in a non-tactic entry *) @@ -167,12 +167,12 @@ let intern_non_tactic_reference strict ist r = with Not_found -> (* By convention, use IntroIdentifier for unbound ident, when not in a def *) match r with - | Ident (loc,id) when not strict -> + | {loc;v=Ident id} when not strict -> let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in TacGeneric ipat | _ -> (* Reference not found *) - error_global_not_found (snd (qualid_of_reference r)) + error_global_not_found (qualid_of_reference r) let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -268,7 +268,7 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent {loc;v=id} -> if !strict_check then (* If in a defined tactic, no intros-until *) - let c, p = intern_constr ist (make @@ CRef (Ident (Loc.tag id), None)) in + let c, p = intern_constr ist (make @@ CRef (make @@ Ident id, None)) in match DAst.get c with | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id) | _ -> clear,ElimOnConstr ((c, p), NoBindings) @@ -276,7 +276,7 @@ let intern_destruction_arg ist = function clear,ElimOnIdent (make ?loc id) let short_name = function - | AN (Ident (loc,id)) when not !strict_check -> Some (make ?loc id) + | {v=AN {loc;v=Ident id}} when not !strict_check -> Some (make ?loc id) | _ -> None let intern_evaluable_global_reference ist r = @@ -284,20 +284,20 @@ let intern_evaluable_global_reference ist r = try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true lqid) with Not_found -> match r with - | Ident (loc,id) when not !strict_check -> EvalVarRef id - | _ -> error_global_not_found (snd lqid) + | {loc;v=Ident id} when not !strict_check -> EvalVarRef id + | _ -> error_global_not_found lqid let intern_evaluable_reference_or_by_notation ist = function - | AN r -> intern_evaluable_global_reference ist r - | ByNotation {loc;v=(ntn,sc)} -> + | {v=AN r} -> intern_evaluable_global_reference ist r + | {v=ByNotation (ntn,sc);loc} -> evaluable_of_global_reference ist.genv (Notation.interp_notation_as_global_reference ?loc (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) (* Globalize a reduction expression *) let intern_evaluable ist = function - | AN (Ident (loc,id)) when find_var id ist -> ArgVar (make ?loc id) - | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist -> + | {loc;v=AN {v=Ident id}} when find_var id ist -> ArgVar (make ?loc id) + | {loc;v=AN {v=Ident id}} when not !strict_check && find_hyp id ist -> ArgArg (EvalVarRef id, Some (make ?loc id)) | r -> let e = intern_evaluable_reference_or_by_notation ist r in @@ -353,10 +353,9 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = ref or a pattern seems interesting, with "head" reduction in case of an evaluable ref, and "strong" reduction in the subterm matched when a pattern *) - let loc = loc_of_smart_reference r in let r = match r with - | AN r -> r - | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in + | {v=AN r} -> r + | {loc} -> make ?loc @@ Qualid (qualid_of_path (path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; @@ -376,7 +375,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = | Inl r -> interp_ref r | Inr { v = CAppExpl((None,r,None),[]) } -> (* We interpret similarly @ref and ref *) - interp_ref (AN r) + interp_ref (make @@ AN r) | Inr c -> Inr (snd (intern_typed_pattern ist ~as_type:false ~ltacvars:ist.ltacvars c))) @@ -385,13 +384,13 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let dump_glob_red_expr = function | Unfold occs -> List.iter (fun (_, r) -> try - Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r) + Dumpglob.add_glob ?loc:r.loc (Smartlocate.smart_global r) with e when CErrors.noncritical e -> ()) occs | Cbv grf | Lazy grf -> List.iter (fun r -> try - Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r) + Dumpglob.add_glob ?loc:r.loc (Smartlocate.smart_global r) with e when CErrors.noncritical e -> ()) grf.rConst | _ -> () diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a287b13b9..6a4bf577b 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -360,7 +360,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found ?loc (qualid_of_ident id) + with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -376,14 +376,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found ?loc (qualid_of_ident id) + | _ -> error_global_not_found (make ?loc @@ qualid_of_ident id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found ?loc (qualid_of_ident id) + with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -642,7 +642,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> - error_global_not_found ?loc (qualid_of_ident id)) + error_global_not_found (make ?loc @@ qualid_of_ident id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p @@ -926,7 +926,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (make ?loc id) else - let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (Ident (loc,id),None))) in + let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (make ?loc @@ Ident id,None))) in let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in (sigma, (c,NoBindings)) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index f049963f1..19abf6780 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -853,7 +853,7 @@ open Util (** Constructors for constr_expr *) let mkCProp loc = CAst.make ?loc @@ CSort GProp let mkCType loc = CAst.make ?loc @@ CSort (GType []) -let mkCVar ?loc id = CAst.make ?loc @@ CRef (Ident (Loc.tag ?loc id), None) +let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None) let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 2f8b8cb02..0d82a9f09 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1165,7 +1165,7 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar END let bvar_lname = let open CAst in function - | { v = CRef (Ident (loc, id), _) } -> CAst.make ?loc @@ Name id + | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id | { loc = loc } -> CAst.make ?loc Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c @@ -1257,7 +1257,7 @@ END let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function - | { CAst.v = CRef (Ident (loc, id), _) } -> CAst.make ?loc id + | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index c3b6a7c59..05dbf0a86 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -432,7 +432,7 @@ END let interp_modloc mr = let interp_mod (_, mr) = - let (loc, qid) = qualid_of_reference mr in + let {CAst.loc=loc; v=qid} = qualid_of_reference mr in try Nametab.full_name_module qid with Not_found -> CErrors.user_err ?loc (str "No Module " ++ pr_qualid qid) in let mr_out, mr_in = List.partition fst mr in @@ -565,9 +565,9 @@ GEXTEND Gram gallina_ext: (* Canonical structure *) [[ IDENT "Canonical"; qid = Constr.global -> - Vernacexpr.VernacCanonical (AN qid) + Vernacexpr.VernacCanonical (CAst.make @@ AN qid) | IDENT "Canonical"; ntn = Prim.by_notation -> - Vernacexpr.VernacCanonical (ByNotation ntn) + Vernacexpr.VernacCanonical (CAst.make @@ ByNotation ntn) | IDENT "Canonical"; qid = Constr.global; d = G_vernac.def_body -> let s = coerce_reference_to_id qid in diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 33b18001c..6a1be9db0 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -131,8 +131,8 @@ let add_genarg tag pr = (** Constructors for cast type *) let dC t = CastConv t (** Constructors for constr_expr *) -let isCVar = function { CAst.v = CRef (Ident _, _) } -> true | _ -> false -let destCVar = function { CAst.v = CRef (Ident (_, id), _) } -> id | _ -> +let isCVar = function { CAst.v = CRef ({CAst.v=Ident _},_) } -> true | _ -> false +let destCVar = function { CAst.v = CRef ({CAst.v=Ident id},_) } -> id | _ -> CErrors.anomaly (str"not a CRef.") let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) @@ -1012,8 +1012,8 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern let id_of_cpattern (_, (c1, c2), _) = let open CAst in match DAst.get c1, c2 with - | _, Some { v = CRef (Ident (_, x), _) } -> Some x - | _, Some { v = CAppExpl ((_, Ident (_, x), _), []) } -> Some x + | _, Some { v = CRef ({CAst.v=Ident x}, _) } -> Some x + | _, Some { v = CAppExpl ((_, {CAst.v=Ident x}, _), []) } -> Some x | GRef (VarRef x, _), None -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 8fab92779..587892141 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -71,17 +71,17 @@ let has_two_constructors lc = let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1 -let encode_bool r = +let encode_bool ({CAst.loc} as r) = let (x,lc) = encode_inductive r in if not (has_two_constructors lc) then - user_err ?loc:(loc_of_reference r) ~hdr:"encode_if" + user_err ?loc ~hdr:"encode_if" (str "This type has not exactly two constructors."); x -let encode_tuple r = +let encode_tuple ({CAst.loc} as r) = let (x,lc) = encode_inductive r in if not (isomorphic_to_tuple lc) then - user_err ?loc:(loc_of_reference r) ~hdr:"encode_tuple" + user_err ?loc ~hdr:"encode_tuple" (str "This type cannot be seen as a tuple type."); x diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4bcb7e459..4962b89a0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -180,20 +180,20 @@ let _ = (** Miscellaneous interpretation functions *) let interp_known_universe_level evd r = - let loc, qid = Libnames.qualid_of_reference r in + let qid = Libnames.qualid_of_reference r in try - match r with - | Libnames.Ident (loc, id) -> Evd.universe_of_name evd id + match r.CAst.v with + | Libnames.Ident id -> Evd.universe_of_name evd id | Libnames.Qualid _ -> raise Not_found with Not_found -> - let univ, k = Nametab.locate_universe qid in + let univ, k = Nametab.locate_universe qid.CAst.v in Univ.Level.make univ k let interp_universe_level_name ~anon_rigidity evd r = try evd, interp_known_universe_level evd r with Not_found -> match r with (* Qualified generated name *) - | Libnames.Qualid (loc, qid) -> + | {CAst.loc; v=Libnames.Qualid qid} -> let dp, i = Libnames.repr_qualid qid in let num = try int_of_string (Id.to_string i) @@ -206,7 +206,7 @@ let interp_universe_level_name ~anon_rigidity evd r = try Evd.add_global_univ evd level with UGraph.AlreadyDeclared -> evd in evd, level - | Libnames.Ident (loc, id) -> (* Undeclared *) + | {CAst.loc; v=Libnames.Ident id} -> (* Undeclared *) if not (is_strict_universe_declarations ()) then new_univ_level_variable ?loc ~name:id univ_rigid evd else user_err ?loc ~hdr:"interp_universe_level_name" diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 8854ff898..412a1cbb4 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -213,9 +213,9 @@ let tag_var = tag Tag.variable let pr_universe_instance l = pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l - let pr_reference = function - | Qualid (_, qid) -> pr_qualid qid - | Ident (_, id) -> tag_var (pr_id id) + let pr_reference = CAst.with_val (function + | Qualid qid -> pr_qualid qid + | Ident id -> tag_var (pr_id id)) let pr_cref ref us = pr_reference ref ++ pr_universe_instance us @@ -565,8 +565,8 @@ let tag_var = tag Tag.variable return (p ++ prlist (pr spc (lapp,L)) l2, lapp) else return (p, lproj) - | CAppExpl ((None,Ident (_,var),us),[t]) - | CApp ((_, {CAst.v = CRef(Ident(_,var),us)}),[t,None]) + | CAppExpl ((None,{v=Ident var},us),[t]) + | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None]) when Id.equal var Notation_ops.ldots_var -> return ( hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), diff --git a/printing/pputils.ml b/printing/pputils.ml index c2846c4cd..c14aa318e 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -123,8 +123,8 @@ let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma) let pr_or_by_notation f = function - | AN v -> f v - | ByNotation {CAst.v=(s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + | {CAst.loc; v=AN v} -> f v + | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let hov_if_not_empty n p = if Pp.ismt p then p else hov n p diff --git a/printing/prettyp.ml b/printing/prettyp.ml index cfc5e6b4e..1f17d844f 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -15,6 +15,7 @@ open Pp open CErrors open Util +open CAst open Names open Nameops open Termops @@ -343,7 +344,7 @@ let register_locatable name f = exception ObjFound of logical_name let locate_any_name ref = - let (loc,qid) = qualid_of_reference ref in + let {v=qid} = qualid_of_reference ref in try Term (Nametab.locate qid) with Not_found -> try Syntactic (Nametab.locate_syndef qid) @@ -452,7 +453,7 @@ type locatable_kind = | LocAny let print_located_qualid name flags ref = - let (loc,qid) = qualid_of_reference ref in + let {v=qid} = qualid_of_reference ref in let located = match flags with | LocTerm -> locate_term qid | LocModule -> locate_modtype qid @ locate_module qid @@ -784,11 +785,11 @@ let print_full_pure_context env sigma = (* This is designed to print the contents of an opened section *) let read_sec_context r = - let loc,qid = qualid_of_reference r in + let qid = qualid_of_reference r in let dir = - try Nametab.locate_section qid + try Nametab.locate_section qid.v with Not_found -> - user_err ?loc ~hdr:"read_sec_context" (str "Unknown section.") in + user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest -> if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest @@ -838,12 +839,12 @@ let print_any_name env sigma na udecl = let print_name env sigma na udecl = match na with - | ByNotation {CAst.loc;v=(ntn,sc)} -> + | {loc; v=ByNotation (ntn,sc)} -> print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl - | AN ref -> + | {loc; v=AN ref} -> print_any_name env sigma (locate_any_name ref) udecl let print_opaque_name env sigma qid = @@ -891,12 +892,12 @@ let print_about_any ?loc env sigma k udecl = let print_about env sigma na udecl = match na with - | ByNotation {CAst.loc;v=(ntn,sc)} -> + | {loc;v=ByNotation (ntn,sc)} -> print_about_any ?loc env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl - | AN ref -> - print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref) udecl + | {loc;v=AN ref} -> + print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) let inspect env sigma depth = diff --git a/printing/printer.ml b/printing/printer.ml index e50d302b3..199aa79c6 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -235,9 +235,9 @@ let qualid_of_global env r = let safe_gen f env sigma c = let orig_extern_ref = Constrextern.get_extern_reference () in let extern_ref ?loc vars r = - try orig_extern_ref ?loc vars r + try orig_extern_ref vars r with e when CErrors.noncritical e -> - Libnames.Qualid (Loc.tag ?loc @@ qualid_of_global env r) + CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r) in Constrextern.set_extern_reference extern_ref; try diff --git a/stm/stm.ml b/stm/stm.ml index b1cecc6d1..ad94b6807 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2571,8 +2571,8 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = let load_objs libs = let rq_file (dir, from, exp) = - let mp = Libnames.(Qualid (Loc.tag @@ qualid_of_string dir)) in - let mfrom = Option.map (fun fr -> Libnames.(Qualid (Loc.tag @@ qualid_of_string fr))) from in + let mp = CAst.make @@ Libnames.(Qualid (qualid_of_string dir)) in + let mfrom = Option.map (fun fr -> CAst.make @@ Libnames.(Qualid (qualid_of_string fr))) from in Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in List.(iter rq_file (rev libs)) in diff --git a/tactics/hints.ml b/tactics/hints.ml index f3e0619a2..a285d6b93 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1279,7 +1279,7 @@ let interp_hints poly = prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in let fref r = let gr = global_with_alias r in - Dumpglob.add_glob ?loc:(loc_of_reference r) gr; + Dumpglob.add_glob ?loc:r.CAst.loc gr; gr in let fr r = evaluable_of_global_reference env (fref r) in let fi c = @@ -1306,7 +1306,7 @@ let interp_hints poly = let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in let mib,_ = Global.lookup_inductive ind in - Dumpglob.dump_reference ?loc:(fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind"; + Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_reference qid) "ind"; List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in diff --git a/vernac/classes.ml b/vernac/classes.ml index e074e44a4..76d427add 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -72,7 +72,7 @@ let existing_instance glob g info = let _, r = Term.decompose_prod_assum instance in match class_of_constr Evd.empty (EConstr.of_constr r) with | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c) - | None -> user_err ?loc:(loc_of_reference g) + | None -> user_err ?loc:g.CAst.loc ~hdr:"declare_instance" (Pp.str "Constant does not build instances of a declared type class.") @@ -227,10 +227,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let sigma, c = interp_casted_constr_evars env' sigma term cty in Some (Inr (c, subst)), sigma | Some (Inl props) -> - let get_id = - function - | Ident (loc, id') -> CAst.(make ?loc @@ id') - | Qualid (loc,id') -> CAst.(make ?loc @@ snd (repr_qualid id')) + let get_id = CAst.map (function + | Ident id' -> id' + | Qualid id' -> snd (repr_qualid id')) in let props, rest = List.fold_left diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index c59286d1a..db2f16525 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -46,8 +46,8 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function user_err ?loc (strbrk"Cannot infer the non constant arguments of the conclusion of " ++ Id.print cs ++ str "."); - let args = List.map (fun id -> CAst.make ?loc @@ CRef(Ident(loc,id),None)) params in - CAppExpl ((None,Ident(loc,name),None),List.rev args) + let args = List.map (fun id -> CAst.(make ?loc @@ CRef(make ?loc @@ Ident id,None))) params in + CAppExpl ((None,CAst.make ?loc @@ Ident name,None),List.rev args) | c -> c ) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index bd7ee0978..b95741ca4 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -44,7 +44,7 @@ let mkSubset sigma name typ prop = let sigT = Lazy.from_fun build_sigma_type -let make_qref s = Qualid (Loc.tag @@ qualid_of_string s) +let make_qref s = CAst.make @@ Qualid (qualid_of_string s) let lt_ref = make_qref "Init.Peano.lt" let rec telescope sigma l = diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 27587416b..32885ab88 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -489,10 +489,9 @@ let do_combined_scheme name schemes = let open CAst in let csts = 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.")) + let qualid = qualid_of_ident v in + try Nametab.locate_constant qualid + with Not_found -> user_err ?loc Pp.(pr_qualid qualid ++ str " is not declared.")) schemes in let sigma,body,typ = build_combined_scheme (Global.env ()) csts in diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index a0baca62b..feeca6075 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1448,7 +1448,7 @@ let add_notation_extra_printing_rule df k v = (* Infix notations *) -let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None) +let inject_var x = CAst.make @@ CRef (CAst.make @@ Ident (Id.of_string x),None) let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = check_infix_modifiers modifiers; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index b3eb13fb7..3dbe8b0c0 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -185,28 +185,28 @@ let print_modules () = let print_module r = - let (loc,qid) = qualid_of_reference r in + let qid = qualid_of_reference r in try - let globdir = Nametab.locate_dir qid in + let globdir = Nametab.locate_dir qid.v in match globdir with DirModule { obj_dir; obj_mp; _ } -> Printmod.print_module (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with - Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) + Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid.v) let print_modtype r = - let (loc,qid) = qualid_of_reference r in + let qid = qualid_of_reference r in try - let kn = Nametab.locate_modtype qid in + let kn = Nametab.locate_modtype qid.v in Printmod.print_modtype kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try - let mp = Nametab.locate_module qid in + let mp = Nametab.locate_module qid.v in Printmod.print_module false mp with Not_found -> - user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) + user_err (str"Unknown Module Type or Module " ++ pr_qualid qid.v) let print_namespace ns = let ns = List.rev (Names.DirPath.repr ns) in @@ -390,7 +390,7 @@ let err_notfound_library ?loc ?from qid = (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library r = - let (loc,qid) = qualid_of_reference r in + let {loc;v=qid} = qualid_of_reference r in try msg_found_library (Library.locate_qualified_library ~warn:false qid) with | Library.LibUnmappedDir -> err_unmapped_library ?loc qid @@ -398,13 +398,13 @@ let print_located_library r = let smart_global r = let gr = Smartlocate.smart_global r in - Dumpglob.add_glob ?loc:(Stdarg.loc_of_or_by_notation loc_of_reference r) gr; - gr + Dumpglob.add_glob ?loc:r.loc gr; + gr let dump_global r = try let gr = Smartlocate.smart_global r in - Dumpglob.add_glob ?loc:(Stdarg.loc_of_or_by_notation loc_of_reference r) gr + Dumpglob.add_glob ?loc:r.loc gr with e when CErrors.noncritical e -> () (**********) (* Syntax *) @@ -640,7 +640,7 @@ let vernac_scheme l = let vernac_combined_scheme lid l = if Dumpglob.dump () then (Dumpglob.dump_definition lid false "def"; - List.iter (fun {loc;v=id} -> dump_global (Misctypes.AN (Ident (Loc.tag ?loc id)))) l); + List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Misctypes.AN (make ?loc @@ Ident id))) l); Indschemes.do_combined_scheme lid l let vernac_universe ~atts l = @@ -679,7 +679,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = in Dumpglob.dump_moddef ?loc mp "mod"; 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 + Option.iter (fun export -> vernac_import export [make @@ Ident id]) export 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) @@ -704,7 +704,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [Ident (Loc.tag id)]) export + (fun export -> vernac_import export [make @@ Ident id]) export ) argsexport | _::_ -> let binders_ast = List.map @@ -719,14 +719,14 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt Dumpglob.dump_moddef ?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 (Loc.tag id)]) + Option.iter (fun export -> vernac_import export [make @@ Ident id]) export 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 (Loc.tag ?loc id)]) export + Option.iter (fun export -> vernac_import export [make ?loc @@ Ident id]) export let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then @@ -751,7 +751,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [Ident (Loc.tag id)]) export + (fun export -> vernac_import export [make ?loc @@ Ident id]) export ) argsexport | _ :: _ -> @@ -817,11 +817,11 @@ let vernac_require from import qidl = let root = match from with | None -> None | Some from -> - let (_, qid) = Libnames.qualid_of_reference from in - let (hd, tl) = Libnames.repr_qualid qid in + let qid = Libnames.qualid_of_reference from in + let (hd, tl) = Libnames.repr_qualid qid.v in Some (Libnames.add_dirpath_suffix hd tl) in - let locate (loc, qid) = + let locate {loc;v=qid} = try let warn = not !Flags.quiet in let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in @@ -832,7 +832,7 @@ let vernac_require from import qidl = in let modrefl = List.map locate qidl in if Dumpglob.dump () then - List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref ?loc dp "lib") qidl (List.map fst modrefl); + List.iter2 (fun {CAst.loc} dp -> Dumpglob.dump_libref ?loc dp "lib") qidl (List.map fst modrefl); Library.require_library_from_dirpath modrefl import (* Coercions and canonical structures *) @@ -1688,10 +1688,10 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = (* FIXME error on non None udecl if we find the hyp. *) let glnumopt = query_command_selector ?loc glopt in let gl,id = - match glnumopt,ref_or_by_not with - | None,AN (Ident (_loc,id)) -> (* goal number not given, catch any failure *) + match glnumopt, ref_or_by_not.v with + | None,AN {v=Ident id} -> (* goal number not given, catch any failure *) (try get_nth_goal 1,id with _ -> raise NoHyp) - | Some n,AN (Ident (_loc,id)) -> (* goal number given, catch if wong *) + | Some n,AN {v=Ident id} -> (* goal number given, catch if wong *) (try get_nth_goal n,id with Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs" @@ -1774,7 +1774,7 @@ let vernac_print ~atts env sigma = | PrintStrategy r -> print_strategy r let global_module r = - let (loc,qid) = qualid_of_reference r in + let {loc;v=qid} = qualid_of_reference r in try Nametab.full_name_module qid with Not_found -> user_err ?loc ~hdr:"global_module" @@ -1858,10 +1858,10 @@ let vernac_search ~atts s gopt r = Search.prioritize_search) pr_search let vernac_locate = function - | LocateAny (AN qid) -> print_located_qualid qid - | LocateTerm (AN qid) -> print_located_term qid - | LocateAny (ByNotation { CAst.v=(ntn, sc)}) (** TODO : handle Ltac notations *) - | LocateTerm (ByNotation { CAst.v=(ntn, sc)}) -> + | LocateAny {v=AN qid} -> print_located_qualid qid + | LocateTerm {v=AN qid} -> print_located_term qid + | LocateAny {v=ByNotation (ntn, sc)} (** TODO : handle Ltac notations *) + | LocateTerm {v=ByNotation (ntn, sc)} -> let _, env = Pfedit.get_current_context () in Notation.locate_notation (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc |