diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-13 00:22:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-18 11:02:58 +0200 |
| commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
| tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc | |
| parent | f08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff) | |
Remove reference name type.
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
93 files changed, 636 insertions, 691 deletions
diff --git a/dev/base_include b/dev/base_include index 574bc097e..6f54ecb24 100644 --- a/dev/base_include +++ b/dev/base_include @@ -229,7 +229,7 @@ let pf_e gl s = let _ = Flags.in_debugger := false let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference - (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));; + (fun ?loc _ r -> Nametab.shortest_qualid_of_global ?loc Id.Set.empty r);; let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc)) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index bb8189efc..f3fc126f9 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,14 @@ ### ML API +Names + +- In `Libnames`, the type `reference` and its two constructors `Qualid` and + `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity, + `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be + replaced by a test using `qualid_is_ident`. Extracting the ident part of a + qualid can be done using `qualid_basename`. + Misctypes - Syntax for universe sorts and kinds has been moved from `Misctypes` diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 10a7a4158..844ad9188 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -549,8 +549,8 @@ let encode_path ?loc prefix mpdir suffix id = | Some (mp,dir) -> (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@ DirPath.repr dir) in - CAst.make ?loc @@ Qualid (make_qualid - (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id) + make_qualid ?loc + (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id let raw_string_of_ref ?loc _ = function | ConstRef cst -> @@ -569,9 +569,9 @@ let raw_string_of_ref ?loc _ = function encode_path ?loc "SECVAR" None [] id let short_string_of_ref ?loc _ = function - | 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))) + | VarRef id -> qualid_of_ident ?loc id + | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst))) + | IndRef (kn,0) -> qualid_of_ident ?loc (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/termops.ml b/engine/termops.ml index eacc36107..2db2e07bf 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -297,7 +297,7 @@ let has_no_evar sigma = with Exit -> false let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd) -let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l +let reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l let pr_evar_universe_context ctx = let open UState in diff --git a/engine/termops.mli b/engine/termops.mli index 255494031..f9aa6ba63 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -282,7 +282,7 @@ val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool val is_Type : Evd.evar_map -> constr -> bool -val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference +val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid (** Combinators on judgments *) diff --git a/engine/uState.ml b/engine/uState.ml index 0e3ecdbf5..81ab3dd66 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -295,15 +295,15 @@ let constrain_variables diff ctx = in { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } -let reference_of_level uctx = +let qualid_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname) + try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> - UnivNames.reference_of_level l + UnivNames.qualid_of_level l let pr_uctx_level uctx l = - Libnames.pr_reference (reference_of_level uctx l) + Libnames.pr_qualid (qualid_of_level uctx l) type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) diff --git a/engine/uState.mli b/engine/uState.mli index e7e5b39e0..a59e61b89 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -171,6 +171,6 @@ val update_sigma_env : t -> Environ.env -> t (** {5 Pretty-printing} *) val pr_uctx_level : t -> Univ.Level.t -> Pp.t -val reference_of_level : t -> Univ.Level.t -> Libnames.reference +val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t diff --git a/engine/univNames.ml b/engine/univNames.ml index 6ffb4bcf0..a68840174 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -14,18 +14,19 @@ open Globnames open Nametab -let reference_of_level l = CAst.make @@ +let qualid_of_level l = match Level.name l with | Some (d, n as na) -> - let qid = - try Nametab.shortest_qualid_of_universe na - with Not_found -> - let name = Id.of_string_soft (string_of_int n) in - Libnames.make_qualid d name - 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) + begin + try Nametab.shortest_qualid_of_universe na + with Not_found -> + let name = Id.of_string_soft (string_of_int n) in + Libnames.make_qualid d name + end + | None -> + Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l) + +let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l) (** Global universe information outside the kernel, to handle polymorphic universe names in sections that have to be discharged. *) diff --git a/engine/univNames.mli b/engine/univNames.mli index c19aa19d5..837beac26 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -11,7 +11,7 @@ open Univ val pr_with_global_universes : Level.t -> Pp.t -val reference_of_level : Level.t -> Libnames.reference +val qualid_of_level : Level.t -> Libnames.qualid (** Global universe information outside the kernel, to handle polymorphic universes in sections that have to be discharged. *) diff --git a/engine/universes.ml b/engine/universes.ml index 70601987c..ee9668433 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -17,7 +17,7 @@ type universe_binders = UnivNames.universe_binders type univ_name_list = UnivNames.univ_name_list let pr_with_global_universes = UnivNames.pr_with_global_universes -let reference_of_level = UnivNames.reference_of_level +let reference_of_level = UnivNames.qualid_of_level let add_global_universe = UnivNames.add_global_universe diff --git a/engine/universes.mli b/engine/universes.mli index 46ff33a47..29673de1e 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -22,8 +22,8 @@ open Univ val pr_with_global_universes : Level.t -> Pp.t [@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"] -val reference_of_level : Level.t -> Libnames.reference -[@@ocaml.deprecated "Use [UnivNames.reference_of_level]"] +val reference_of_level : Level.t -> Libnames.qualid +[@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"] val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit [@@ocaml.deprecated "Use [UnivNames.add_global_universe]"] diff --git a/ide/idetop.ml b/ide/idetop.ml index ba69c4185..7abbf239b 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -290,8 +290,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 {CAst.v=qid} = Libnames.qualid_of_reference m in + let qid = Pcoq.parse_string Pcoq.Constr.global path in let id = try Nametab.full_name_module qid with Not_found -> diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index d725f5afa..521eeb8e9 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -61,17 +61,17 @@ type instance_expr = Glob_term.glob_level list type cases_pattern_expr_r = | CPatAlias of cases_pattern_expr * lname - | CPatCstr of reference + | CPatCstr of qualid * cases_pattern_expr list option * cases_pattern_expr list (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) - | CPatAtom of reference option + | CPatAtom of qualid option | CPatOr of cases_pattern_expr list | CPatNotation of notation * cases_pattern_notation_substitution * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2 *) | CPatPrim of prim_token - | CPatRecord of (reference * cases_pattern_expr) list + | CPatRecord of (qualid * cases_pattern_expr) list | CPatDelimiters of string * cases_pattern_expr | CPatCast of cases_pattern_expr * constr_expr and cases_pattern_expr = cases_pattern_expr_r CAst.t @@ -81,16 +81,16 @@ and cases_pattern_notation_substitution = cases_pattern_expr list list (** for recursive notations *) and constr_expr_r = - | CRef of reference * instance_expr option + | CRef of qualid * instance_expr option | CFix of lident * fix_expr list | CCoFix of lident * cofix_expr list | CProdN of local_binder_expr list * constr_expr | CLambdaN of local_binder_expr list * constr_expr | CLetIn of lname * constr_expr * constr_expr option * constr_expr - | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list + | CAppExpl of (proj_flag * qualid * instance_expr option) * constr_expr list | CApp of (proj_flag * constr_expr) * (constr_expr * explicitation CAst.t option) list - | CRecord of (reference * constr_expr) list + | CRecord of (qualid * constr_expr) list (* representation of the "let" and "match" constructs *) | CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *) @@ -111,7 +111,7 @@ and constr_expr_r = | CGeneralization of binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr - | CProj of reference * constr_expr + | CProj of qualid * constr_expr and constr_expr = constr_expr_r CAst.t and case_expr = constr_expr (* expression that is being matched *) @@ -150,7 +150,7 @@ type constr_pattern_expr = constr_expr (** Concrete syntax for modules and module types *) type with_declaration_ast = - | CWith_Module of Id.t list CAst.t * qualid CAst.t + | CWith_Module of Id.t list CAst.t * qualid | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr type module_ast_r = diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index d626630ef..4b1af9147 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -10,7 +10,6 @@ open Pp open Util -open CAst open Names open Nameops open Libnames @@ -73,11 +72,11 @@ let rec cases_pattern_expr_eq p1 p2 = | CPatAlias(a1,i1), CPatAlias(a2,i2) -> eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> - eq_reference c1 c2 && + qualid_eq c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && List.equal cases_pattern_expr_eq b1 b2 | CPatAtom(r1), CPatAtom(r2) -> - Option.equal eq_reference r1 r2 + Option.equal qualid_eq r1 r2 | CPatOr a1, CPatOr a2 -> List.equal cases_pattern_expr_eq a1 a2 | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) -> @@ -88,7 +87,7 @@ let rec cases_pattern_expr_eq p1 p2 = prim_token_eq i1 i2 | CPatRecord l1, CPatRecord l2 -> let equal (r1, e1) (r2, e2) = - eq_reference r1 r2 && cases_pattern_expr_eq e1 e2 + qualid_eq r1 r2 && cases_pattern_expr_eq e1 e2 in List.equal equal l1 l2 | CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) -> @@ -108,7 +107,7 @@ let eq_universes u1 u2 = let rec constr_expr_eq e1 e2 = if CAst.(e1.v == e2.v) then true else match CAst.(e1.v, e2.v) with - | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2 + | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2 | CFix(id1,fl1), CFix(id2,fl2) -> eq_ast Id.equal id1 id2 && List.equal fix_expr_eq fl1 fl2 @@ -128,7 +127,7 @@ let rec constr_expr_eq e1 e2 = constr_expr_eq b1 b2 | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) -> Option.equal Int.equal proj1 proj2 && - eq_reference r1 r2 && + qualid_eq r1 r2 && List.equal constr_expr_eq al1 al2 | CApp((proj1,e1),al1), CApp((proj2,e2),al2) -> Option.equal Int.equal proj1 proj2 && @@ -136,7 +135,7 @@ let rec constr_expr_eq e1 e2 = List.equal args_eq al1 al2 | CRecord l1, CRecord l2 -> let field_eq (r1, e1) (r2, e2) = - eq_reference r1 r2 && constr_expr_eq e1 e2 + qualid_eq r1 r2 && constr_expr_eq e1 e2 in List.equal field_eq l1 l2 | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> @@ -178,7 +177,7 @@ let rec constr_expr_eq e1 e2 = String.equal s1 s2 && constr_expr_eq e1 e2 | CProj(p1,c1), CProj(p2,c2) -> - eq_reference p1 p2 && constr_expr_eq c1 c2 + qualid_eq p1 p2 && constr_expr_eq c1 c2 | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _ | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _ | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _ @@ -280,7 +279,9 @@ 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 {v=Ident id}) when not (is_constructor id) -> f id a + | CPatAtom (Some qid) + when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) -> + f (qualid_basename qid) a | CPatPrim _ | CPatAtom _ -> a | CPatCast ({CAst.loc},_) -> CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names" @@ -363,7 +364,9 @@ 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 ({v=Ident id},_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + let id = qualid_basename qid in + 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 @@ -440,11 +443,13 @@ 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 ({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 +let rec replace_vars_constr_expr l r = + match r with + | { CAst.loc; v = CRef (qid,us) } as x when qualid_is_ident qid -> + let id = qualid_basename qid in + (try CAst.make ?loc @@ CRef (qualid_of_ident ?loc (Id.Map.find id l),us) + with Not_found -> x) + | cn -> map_constr_expr_with_binders Id.Map.remove replace_vars_constr_expr l cn (* Returns the ranges of locs of the notation that are not occupied by args *) (* and which are then occupied by proper symbols of the notation (or spaces) *) @@ -513,7 +518,7 @@ let split_at_annot bl na = (** Pseudo-constructors *) -let mkIdentC id = CAst.make @@ CRef (make @@ Ident id,None) +let mkIdentC id = CAst.make @@ CRef (qualid_of_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) @@ -532,20 +537,22 @@ let mkCProdN ?loc bll c = let mkCLambdaN ?loc bll c = CAst.make ?loc @@ CLambdaN (bll,c) -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.")) +let coerce_reference_to_id qid = + if qualid_is_ident qid then qualid_basename qid + else + CErrors.user_err ?loc:qid.CAst.loc ~hdr:"coerce_reference_to_id" + (str "This expression should be a simple identifier.") let coerce_to_id = function - | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc id + | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid -> + CAst.make ?loc @@ qualid_basename qid | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_id" (str "This expression should be a simple identifier.") let coerce_to_name = function - | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id + | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid -> + CAst.make ?loc @@ Name (qualid_basename qid) | { CAst.loc; v = CHole (None,IntroAnonymous,None) } -> CAst.make ?loc Anonymous | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") @@ -572,7 +579,8 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function CPatAtom (Some r) | CHole (None,IntroAnonymous,None) -> CPatAtom None - | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' -> + | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (qid,None) }) + when qualid_is_ident qid && Id.equal id (qualid_basename qid) -> 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/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 1c2348457..46aef1c78 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -41,7 +41,7 @@ val local_binders_loc : local_binder_expr list -> Loc.t option (** {6 Constructors}*) val mkIdentC : Id.t -> constr_expr -val mkRefC : reference -> constr_expr +val mkRefC : qualid -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr @@ -61,7 +61,7 @@ val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list - (** {6 Destructors}*) -val coerce_reference_to_id : reference -> Id.t +val coerce_reference_to_id : qualid -> Id.t (** FIXME: nothing to do here *) val coerce_to_id : constr_expr -> lident diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c613effcd..2538c7772 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -270,7 +270,7 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - make @@ Qualid (shortest_qualid_of_global vars r) + shortest_qualid_of_global ?loc vars r let my_extern_reference = ref default_extern_reference @@ -388,7 +388,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 (make ?loc @@ Ident id)) + | PatVar (Name id) -> CPatAtom (Some (qualid_of_ident ?loc id)) | PatVar (Anonymous) -> CPatAtom None | PatCstr(cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes vars) args in @@ -457,7 +457,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 = make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn) in + let qid = shortest_qualid_of_syndef ?loc 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 (make ?loc @@ Ident id)) + | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id)) with No_match -> extern_notation_pattern allscopes vars t rules @@ -753,7 +753,7 @@ let rec extern inctx scopes vars r = extern_global (select_stronger_impargs (implicits_of_global ref)) (extern_reference vars ref) (extern_universes us) - | GVar id -> CRef (make ?loc @@ Ident id,None) + | GVar id -> CRef (qualid_of_ident ?loc id,None) | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None) @@ -1095,7 +1095,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 (make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn),None) in + let a = CRef (shortest_qualid_of_syndef ?loc 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/constrextern.mli b/interp/constrextern.mli index 73c108319..f09b316cd 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -38,7 +38,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr -val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference +val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> @@ -56,9 +56,9 @@ val print_projections : bool ref (** Customization of the global_reference printer *) val set_extern_reference : - (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) -> unit + (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid) -> unit val get_extern_reference : - unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) + unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid) (** WARNING: The following functions are evil due to side-effects. Think of the following case as used in the printer: diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 47ae64d47..4e217b2cd 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -96,8 +96,8 @@ let is_global id = with Not_found -> false -let global_reference_of_reference ref = - locate_reference (qualid_of_reference ref).CAst.v +let global_reference_of_reference qid = + locate_reference qid let global_reference id = locate_reference (qualid_of_ident id) @@ -117,7 +117,7 @@ let global_reference_in_absolute_module dir id = type internalization_error = | VariableCapture of Id.t * Id.t | IllegalMetavariable - | NotAConstructor of reference + | NotAConstructor of qualid | UnboundFixName of bool * Id.t | NonLinearPattern of Id.t | BadPatternsNumber of int * int @@ -131,8 +131,8 @@ let explain_variable_capture id id' = let explain_illegal_metavariable = str "Metavariables allowed only in patterns" -let explain_not_a_constructor ref = - str "Unknown constructor: " ++ pr_reference ref +let explain_not_a_constructor qid = + str "Unknown constructor: " ++ pr_qualid qid let explain_unbound_fix_name is_cofix id = str "The name" ++ spc () ++ Id.print id ++ @@ -404,7 +404,8 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars let name = let id = match ty with - | { v = CApp ((_, { v = CRef ({v=Ident id},_) } ), _) } -> id + | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> + qualid_basename qid | _ -> default_non_dependent_ident in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name @@ -556,7 +557,8 @@ let is_var store pat = let out_var pat = match pat.v with - | CPatAtom (Some ({v=Ident id})) -> Name id + | CPatAtom (Some qid) when qualid_is_ident qid -> + Name (qualid_basename qid) | CPatAtom None -> Anonymous | _ -> assert false @@ -622,18 +624,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 (make @@ Ident id, None) + | PatVar (Name id) -> CRef (qualid_of_ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in + let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,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 + CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with | bnd :: l -> let loc = bnd.loc in begin match DAst.get bnd with - | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (make ?loc @@ Ident id, None)) :: extract_variables l + | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l | GLocalDef (Name id,_,_,_) -> extract_variables l | GLocalDef (Anonymous,_,_,_) | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.") @@ -806,7 +808,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 (make ?loc @@ Ident id) | Anonymous -> None in + let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in CAst.make ?loc (CPatAtom atom) let split_by_type ids subst = @@ -903,7 +905,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 (make ?loc @@ Ident id,None), Some (make ?loc @@ ExplByName id)) expl_impls in + (fun id -> CAst.make ?loc @@ CRef (qualid_of_ident ?loc 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 @@ -970,18 +972,17 @@ 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;v=qid} = - let r = Nametab.locate_extended qid in dump_extended_global loc r; r +let intern_extended_global_of_qualid qid = + let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r -let intern_reference ref = - let qid = qualid_of_reference ref in +let intern_reference qid = let r = try intern_extended_global_of_qualid qid with Not_found -> error_global_not_found qid in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option = +let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option = match info with | UAnonymous -> None | UUnknown -> None @@ -1014,7 +1015,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in let loc = c.loc in let err () = - user_err ?loc (str "Notation " ++ pr_qualid qid.v + user_err ?loc (str "Notation " ++ pr_qualid qid ++ str " cannot have a universe instance," ++ str " its expanded head does not start with a reference") in @@ -1031,34 +1032,32 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = | Some [s], GSort (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.v) + user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) | Some _, _ -> err () in c, projapp, args2 -let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = -function - | {loc; v=Qualid qid} -> - let qid = make ?loc qid in - let r,projapp,args2 = - 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 - | {loc; v=Ident id} -> - try intern_var env lvar namedctx loc id us, args +let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qid = + let loc = qid.CAst.loc in + if qualid_is_ident qid then + try intern_var env lvar namedctx loc (qualid_basename qid) us, args with Not_found -> - let qid = make ?loc @@ qualid_of_ident id in try let r, projapp, args2 = intern_qualid ~no_secvar:true 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 + (* Extra allowance for non globalizing functions *) + if !interning_grammar || env.unb then + (gvar (loc,qualid_basename qid) us, [], [], []), args else error_global_not_found qid + else + let r,projapp,args2 = + 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 let interp_reference vars r = let (r,_,_,_),_ = @@ -1262,18 +1261,18 @@ let find_constructor loc add_params ref = List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)]) | None -> [] -let find_pattern_variable = function - | {v=Ident id} -> id - | {loc;v=Qualid _} as x -> raise (InternalizationError(loc,NotAConstructor x)) +let find_pattern_variable qid = + if qualid_is_ident qid then qualid_basename qid + else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid)) let check_duplicate loc fields = - let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in + let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in let dups = List.duplicates eq fields in match dups with | [] -> () | (r, _) :: _ -> user_err ?loc (str "This record defines several times the field " ++ - pr_reference r ++ str ".") + pr_qualid r ++ str ".") (** [sort_fields ~complete loc fields completer] expects a list [fields] of field assignments [f = e1; g = e2; ...], where [f, g] @@ -1298,14 +1297,14 @@ let sort_fields ~complete loc fields completer = (gr, Recordops.find_projection gr) with Not_found -> user_err ?loc ~hdr:"intern" - (pr_reference first_field_ref ++ str": Not a projection") + (pr_qualid first_field_ref ++ str": Not a projection") in (* the number of parameters *) let nparams = record.Recordops.s_EXPECTEDPARAM in (* the reference constructor of the record *) let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in - try make ?loc @@ Qualid (shortest_qualid_of_global Id.Set.empty global_record_id) + try shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in @@ -1356,7 +1355,7 @@ let sort_fields ~complete loc fields completer = let field_glob_ref = try global_reference_of_reference field_ref with Not_found -> user_err ?loc ~hdr:"intern" - (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in + (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in let remaining_projs, (field_index, _) = let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in try CList.extract_first the_proj remaining_projs @@ -1483,10 +1482,9 @@ let drop_notations_pattern looked_for genv = end | _ -> 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 qid = qualid_of_reference re in + let rec drop_syndef top scopes qid pats = try - match locate_extended qid.v with + match locate_extended qid with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with @@ -1542,10 +1540,10 @@ let drop_notations_pattern looked_for genv = | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (r, Some expl_pl, pl) -> - let g = try locate (qualid_of_reference r).v + | CPatCstr (qid, Some expl_pl, pl) -> + let g = try locate qid with Not_found -> - raise (InternalizationError (loc,NotAConstructor r)) in + raise (InternalizationError (loc,NotAConstructor qid)) in if expl_pl == [] then (* Convention: (@r) deactivates all further implicit arguments and scopes *) DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, []) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 12f77af30..dd0944cc4 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -141,10 +141,10 @@ val intern_constr_pattern : constr_pattern_expr -> patvar list * constr_pattern (** Raise Not_found if syndef not bound to a name and error if unexisting ref *) -val intern_reference : reference -> GlobRef.t +val intern_reference : qualid -> GlobRef.t (** Expands abbreviations (syndef); raise an error if not existing *) -val interp_reference : ltac_sign -> reference -> glob_constr +val interp_reference : ltac_sign -> qualid -> glob_constr (** Interpret binders *) diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml index 42c1fe429..607f2258f 100644 --- a/interp/genredexpr.ml +++ b/interp/genredexpr.ml @@ -60,6 +60,6 @@ open Constrexpr type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation +type r_cst = qualid or_by_notation type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index b54e2badd..83ad9af33 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -96,9 +96,11 @@ 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 ({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 + | CRef (qid,_) when qualid_is_ident qid -> + found c.CAst.loc (qualid_basename qid) bdvars l + | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when + qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) -> + Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) 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 @@ -196,7 +198,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 (CAst.make @@ Ident id',None), Id.Set.add id' avoid) + (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) let destClassApp cl = let open CAst in @@ -218,9 +220,8 @@ let destClassAppExpl cl = let implicit_application env ?(allow_partial=true) f ty = let is_class = try - let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in - let qid = qualid_of_reference r in - let gr = Nametab.locate qid.CAst.v in + let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in + let gr = Nametab.locate qid in if Typeclasses.is_class gr then Some (clapp, gr) else None with Not_found -> None in diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 25394fc0d..a8492095e 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -16,8 +16,8 @@ open Libnames val declare_generalizable : local:bool -> lident list option -> unit val ids_of_list : Id.t list -> Id.Set.t -val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t -val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t +val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t +val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t (** Fragile, should be used only for construction a set of identifiers to avoid *) diff --git a/interp/modintern.ml b/interp/modintern.ml index 33c07d551..c27cc9cc0 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -45,8 +45,9 @@ let error_application_to_module_type loc = or both are searched. The returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) -let lookup_module_or_modtype kind {CAst.loc;v=qid} = +let lookup_module_or_modtype kind qid = let open Declaremods in + let loc = qid.CAst.loc in try if kind == ModType then raise Not_found; let mp = Nametab.locate_module qid in @@ -84,7 +85,7 @@ let loc_of_module l = l.CAst.loc let rec interp_module_ast env kind m cst = match m with | {CAst.loc;v=CMident qid} -> - let (mp,kind) = lookup_module_or_modtype kind CAst.(make ?loc qid) in + let (mp,kind) = lookup_module_or_modtype kind qid in (MEident mp, kind, cst) | {CAst.loc;v=CMapply (me1,me2)} -> let me1',kind1, cst = interp_module_ast env kind me1 cst in diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index e1fbdba87..91491bdf8 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -41,26 +41,24 @@ let global_of_extended_global = function | [],NApp (NRef ref,[]) -> ref | _ -> raise Not_found -let locate_global_with_alias ?(head=false) {CAst.loc; v=qid} = +let locate_global_with_alias ?(head=false) 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:qid.CAst.loc (pr_qualid qid ++ str " is bound to a notation that does not denote a reference.") -let global_inductive_with_alias ({CAst.loc} as lr) = - let qid = qualid_of_reference lr in +let global_inductive_with_alias qid = try match locate_global_with_alias qid with | IndRef ind -> ind | ref -> - user_err ?loc ~hdr:"global_inductive" - (pr_reference lr ++ spc () ++ str "is not an inductive type.") + user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" + (pr_qualid qid ++ spc () ++ str "is not an inductive type.") with Not_found -> Nametab.error_global_not_found qid -let global_with_alias ?head r = - let qid = qualid_of_reference r in +let global_with_alias ?head qid = try locate_global_with_alias ?head qid with Not_found -> Nametab.error_global_not_found qid diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 6b574d7b5..e41ef7891 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -17,7 +17,7 @@ open Globnames 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 CAst.t -> GlobRef.t +val locate_global_with_alias : ?head:bool -> qualid -> GlobRef.t (** Extract a global_reference from a reference that can be an "alias" *) val global_of_extended_global : extended_global_reference -> GlobRef.t @@ -26,13 +26,13 @@ val global_of_extended_global : extended_global_reference -> GlobRef.t May raise [Nametab.GlobalizationError _] for an unknown reference, or a [UserError] if bound to a syntactic def that does not denote a reference. *) -val global_with_alias : ?head:bool -> reference -> GlobRef.t +val global_with_alias : ?head:bool -> qualid -> GlobRef.t (** The same for inductive types *) -val global_inductive_with_alias : reference -> inductive +val global_inductive_with_alias : qualid -> inductive (** Locate a reference taking into account notations and "aliases" *) -val smart_global : ?head:bool -> reference Constrexpr.or_by_notation -> GlobRef.t +val smart_global : ?head:bool -> qualid Constrexpr.or_by_notation -> GlobRef.t (** The same for inductive types *) -val smart_global_inductive : reference Constrexpr.or_by_notation -> inductive +val smart_global_inductive : qualid Constrexpr.or_by_notation -> inductive diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 4792cda08..5e5e43ed3 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -41,7 +41,7 @@ val wit_ident : Id.t uniform_genarg_type val wit_var : (lident, lident, Id.t) genarg_type -val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_sort_family : (Sorts.family, unit, unit) genarg_type @@ -53,7 +53,7 @@ val wit_open_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type val wit_red_expr : - ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type @@ -63,10 +63,10 @@ val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr, val wit_integer : int uniform_genarg_type val wit_preident : string uniform_genarg_type -val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type -val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_global : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type val wit_redexpr : - ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type diff --git a/library/goptions.ml b/library/goptions.ml index 76071ebcc..f14ad333e 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -161,7 +161,7 @@ module type RefConvertArg = sig type t val compare : t -> t -> int - val encode : reference -> t + val encode : qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name @@ -172,7 +172,7 @@ end module RefConvert = functor (A : RefConvertArg) -> struct type t = A.t - type key = reference + type key = qualid let compare = A.compare let table = ref_table let encode = A.encode diff --git a/library/goptions.mli b/library/goptions.mli index 6c14d19ee..3d7df18fe 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -89,7 +89,7 @@ module MakeRefTable : (A : sig type t val compare : t -> t -> int - val encode : reference -> t + val encode : qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name @@ -147,9 +147,9 @@ val get_string_table : val get_ref_table : option_name -> - < add : reference -> unit; - remove : reference -> unit; - mem : reference -> unit; + < add : qualid -> unit; + remove : qualid -> unit; + mem : qualid -> unit; print : unit > (** The first argument is a locality flag. *) diff --git a/library/libnames.ml b/library/libnames.ml index 8d5a02a29..23085048a 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -134,23 +134,33 @@ let restrict_path n sp = make_path (DirPath.make dir') s (*s qualified names *) -type qualid = full_path +type qualid_r = full_path +type qualid = qualid_r CAst.t -let make_qualid = make_path -let repr_qualid = repr_path +let make_qualid ?loc pa id = CAst.make ?loc (make_path pa id) +let repr_qualid {CAst.v=qid} = repr_path qid -let qualid_eq = eq_full_path +let qualid_eq qid1 qid2 = eq_full_path qid1.CAst.v qid2.CAst.v -let string_of_qualid = string_of_path -let pr_qualid = pr_path +let string_of_qualid qid = string_of_path qid.CAst.v +let pr_qualid qid = pr_path qid.CAst.v -let qualid_of_string = path_of_string +let qualid_of_string ?loc s = CAst.make ?loc @@ path_of_string s -let qualid_of_path sp = sp -let qualid_of_ident id = make_qualid DirPath.empty id -let qualid_of_dirpath dir = +let qualid_of_path ?loc sp = CAst.make ?loc sp +let qualid_of_ident ?loc id = make_qualid ?loc DirPath.empty id +let qualid_of_dirpath ?loc dir = let (l,a) = split_dirpath dir in - make_qualid l a + make_qualid ?loc l a + +let qualid_is_ident qid = + DirPath.is_empty qid.CAst.v.dirpath + +let qualid_basename qid = + qid.CAst.v.basename + +let qualid_path qid = + qid.CAst.v.dirpath type object_name = full_path * KerName.t @@ -183,52 +193,6 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with | DirModule op1, DirModule op2 -> eq_op op1 op2 | _ -> false -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 {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 q2 -> - let (dp1,id1) = repr_qualid q1 in - let (dp2,id2) = repr_qualid q2 in - Qualid (make_qualid - (append_dirpath (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) dp2) - id2) - | Qualid q1, Ident id2 -> - let (dp1,id1) = repr_qualid q1 in - Qualid (make_qualid - (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) - id2) - | Ident id1, Qualid q2 -> - let (dp2,id2) = repr_qualid q2 in - Qualid (make_qualid - (append_dirpath (dirpath_of_string (Names.Id.to_string id1)) dp2) - id2) - | 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 5f69b1f0f..447eecbb5 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -65,23 +65,28 @@ val restrict_path : int -> full_path -> full_path qualifications of absolute names, including single identifiers. The [qualid] are used to access the name table. *) -type qualid +type qualid_r +type qualid = qualid_r CAst.t -val make_qualid : DirPath.t -> Id.t -> qualid +val make_qualid : ?loc:Loc.t -> DirPath.t -> Id.t -> qualid val repr_qualid : qualid -> DirPath.t * Id.t val qualid_eq : qualid -> qualid -> bool val pr_qualid : qualid -> Pp.t val string_of_qualid : qualid -> string -val qualid_of_string : string -> qualid +val qualid_of_string : ?loc:Loc.t -> string -> qualid (** Turns an absolute name, a dirpath, or an Id.t into a qualified name denoting the same name *) -val qualid_of_path : full_path -> qualid -val qualid_of_dirpath : DirPath.t -> qualid -val qualid_of_ident : Id.t -> qualid +val qualid_of_path : ?loc:Loc.t -> full_path -> qualid +val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid +val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid + +val qualid_is_ident : qualid -> bool +val qualid_path : qualid -> DirPath.t +val qualid_basename : qualid -> Id.t (** Both names are passed to objects: a "semantic" [kernel_name], which can be substituted and a "syntactic" [full_path] which can be printed @@ -124,20 +129,6 @@ val eq_global_dir_reference : global_dir_reference -> global_dir_reference -> bool (** {6 ... } *) -(** A [reference] is the user-level notion of name. It denotes either a - global name (referred either by a qualified name or by a single - name) or a variable *) - -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 CAst.t -val string_of_reference : reference -> string -val pr_reference : reference -> Pp.t -val join_reference : reference -> reference -> reference (** some preset paths *) val default_library : DirPath.t diff --git a/library/library.ml b/library/library.ml index 56d2709d5..400f3dcf1 100644 --- a/library/library.ml +++ b/library/library.ml @@ -577,10 +577,10 @@ let require_library_from_dirpath modrefl export = (* the function called by Vernacentries.vernac_import *) -let safe_locate_module {CAst.loc;v=qid} = +let safe_locate_module qid = try Nametab.locate_module qid with Not_found -> - user_err ?loc ~hdr:"import_library" + user_err ?loc:qid.CAst.loc ~hdr:"import_library" (pr_qualid qid ++ str " is not a module") let import_module export modl = @@ -595,18 +595,18 @@ let import_module export modl = | [] -> () | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in let rec aux acc = function - | ({CAst.loc; v=dir} as m) :: l -> + | qid :: l -> let m,acc = - try Nametab.locate_module dir, acc - with Not_found-> flush acc; safe_locate_module m, [] in + try Nametab.locate_module qid, acc + with Not_found-> flush acc; safe_locate_module qid, [] in (match m with | MPfile dir -> aux (dir::acc) l | mp -> flush acc; try Declaremods.import_module export mp; aux [] l with Not_found -> - user_err ?loc ~hdr:"import_library" - (pr_qualid dir ++ str " is not a module")) + user_err ?loc:qid.CAst.loc ~hdr:"import_library" + (pr_qualid qid ++ str " is not a module")) | [] -> flush acc in aux [] modl diff --git a/library/library.mli b/library/library.mli index 0877ebb5a..d5815afc4 100644 --- a/library/library.mli +++ b/library/library.mli @@ -36,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 CAst.t list -> unit +val import_module : bool -> qualid 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 995f44706..a3b3ca6e7 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -18,8 +18,8 @@ open Globnames exception GlobalizationError of qualid -let error_global_not_found {CAst.loc;v} = - Loc.raise ?loc (GlobalizationError v) +let error_global_not_found qid = + Loc.raise ?loc:qid.CAst.loc (GlobalizationError qid) (* The visibility can be registered either - for all suffixes not shorter then a given int - when the object @@ -69,7 +69,7 @@ module type NAMETREE = sig val find : user_name -> t -> elt val exists : user_name -> t -> bool val user_name : qualid -> t -> user_name - val shortest_qualid : Id.Set.t -> user_name -> t -> qualid + val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list end @@ -220,7 +220,7 @@ let exists uname tab = with Not_found -> false -let shortest_qualid ctx uname tab = +let shortest_qualid ?loc ctx uname tab = let id,dir = U.repr uname in let hidden = Id.Set.mem id ctx in let rec find_uname pos dir tree = @@ -235,7 +235,7 @@ let shortest_qualid ctx uname tab = in let ptab = Id.Map.find id tab in let found_dir = find_uname [] dir ptab in - make_qualid (DirPath.make found_dir) id + make_qualid ?loc (DirPath.make found_dir) id let push_node node l = match node with @@ -458,14 +458,13 @@ let global_of_path sp = let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab -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 +let global qid = + try match locate_extended qid with | TrueGlobal ref -> ref | SynDef _ -> - user_err ?loc ~hdr:"global" + user_err ?loc:qid.CAst.loc ~hdr:"global" (str "Unexpected reference to a notation: " ++ - pr_qualid v) + pr_qualid qid) with Not_found -> error_global_not_found qid @@ -510,40 +509,40 @@ let path_of_universe mp = (* Shortest qualid functions **********************************************) -let shortest_qualid_of_global ctx ref = +let shortest_qualid_of_global ?loc ctx ref = match ref with - | VarRef id -> make_qualid DirPath.empty id + | VarRef id -> make_qualid ?loc DirPath.empty id | _ -> let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in - ExtRefTab.shortest_qualid ctx sp !the_ccitab + ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab -let shortest_qualid_of_syndef ctx kn = +let shortest_qualid_of_syndef ?loc ctx kn = let sp = path_of_syndef kn in - ExtRefTab.shortest_qualid ctx sp !the_ccitab + ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab -let shortest_qualid_of_module mp = +let shortest_qualid_of_module ?loc mp = let dir = MPmap.find mp !the_modrevtab in - DirTab.shortest_qualid Id.Set.empty dir !the_dirtab + DirTab.shortest_qualid ?loc Id.Set.empty dir !the_dirtab -let shortest_qualid_of_modtype kn = +let shortest_qualid_of_modtype ?loc kn = let sp = MPmap.find kn !the_modtyperevtab in - MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab + MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab -let shortest_qualid_of_universe kn = +let shortest_qualid_of_universe ?loc kn = let sp = UnivIdMap.find kn !the_univrevtab in - UnivTab.shortest_qualid Id.Set.empty sp !the_univtab + UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global 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 ({CAst.loc; v=r} as lr) = - match global lr with +let global_inductive qid = + match global qid with | IndRef ind -> ind | ref -> - user_err ?loc ~hdr:"global_inductive" - (pr_reference lr ++ spc () ++ str "is not an inductive type") + user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" + (pr_qualid qid ++ spc () ++ str "is not an inductive type") (********************************************************************) diff --git a/library/nametab.mli b/library/nametab.mli index 2ec73a986..57e9141db 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 : qualid CAst.t -> 'a +val error_global_not_found : qualid -> 'a (** {6 Register visibility of things } *) @@ -105,8 +105,8 @@ val locate_universe : qualid -> universe_id references, like [locate] and co, but raise a nice error message in case of failure *) -val global : reference -> GlobRef.t -val global_inductive : reference -> inductive +val global : qualid -> GlobRef.t +val global_inductive : qualid -> inductive (** These functions locate all global references with a given suffix; if [qualid] is valid as such, it comes first in the list *) @@ -168,11 +168,11 @@ val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t Coq.A.B.x that denotes the same object. @raise Not_found for unknown objects. *) -val shortest_qualid_of_global : Id.Set.t -> GlobRef.t -> qualid -val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid -val shortest_qualid_of_modtype : ModPath.t -> qualid -val shortest_qualid_of_module : ModPath.t -> qualid -val shortest_qualid_of_universe : universe_id -> qualid +val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid +val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid +val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid +val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid +val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid (** Deprecated synonyms *) @@ -207,7 +207,7 @@ module type NAMETREE = sig val find : user_name -> t -> elt val exists : user_name -> t -> bool val user_name : qualid -> t -> user_name - val shortest_qualid : Id.Set.t -> user_name -> t -> qualid + val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list end diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 94149a085..1fa26b455 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -202,11 +202,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 (CAst.make ?loc:x.CAst.loc @@ Ident x.CAst.v, None), None) args in + let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc 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, CAst.make ~loc:!@loc @@ Ident ldots_var, None),[c]) ] + CAst.make ~loc:!@loc @@ CAppExpl ((None, (qualid_of_ident ~loc:!@loc 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 08bcd0f8c..91dce27fe 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -18,7 +18,7 @@ let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] let _ = List.iter CLexer.add_keyword prim_kw -let local_make_qualid l id = make_qualid (DirPath.make l) id +let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id let my_int_of_string loc s = try @@ -67,8 +67,8 @@ GEXTEND Gram ] ] ; basequalid: - [ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id' - | id = ident -> qualid_of_ident id + [ [ id = ident; (l,id')=fields -> local_make_qualid !@loc (l@[id]) id' + | id = ident -> qualid_of_ident ~loc:!@loc id ] ] ; name: @@ -77,8 +77,8 @@ GEXTEND Gram ; reference: [ [ id = ident; (l,id') = fields -> - CAst.make ~loc:!@loc @@ Qualid (local_make_qualid (l@[id]) id') - | id = ident -> CAst.make ~loc:!@loc @@ Ident id + local_make_qualid !@loc (l@[id]) id' + | id = ident -> local_make_qualid !@loc [] id ] ] ; by_notation: @@ -89,7 +89,7 @@ GEXTEND Gram | ntn = by_notation -> CAst.make ~loc:!@loc @@ Constrexpr.ByNotation ntn ] ] ; qualid: - [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ] + [ [ qid = basequalid -> qid ] ] ; ne_string: [ [ s = STRING -> diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 9a45bc973..f959bd80c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -213,11 +213,11 @@ module Prim : val integer : int Gram.entry val string : string Gram.entry val lstring : lstring Gram.entry - val qualid : qualid CAst.t Gram.entry + val reference : qualid Gram.entry + val qualid : qualid Gram.entry val fullyqualid : Id.t list CAst.t Gram.entry - val reference : reference Gram.entry val by_notation : (string * string option) Gram.entry - val smart_global : reference or_by_notation Gram.entry + val smart_global : qualid or_by_notation Gram.entry val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry val ne_lstring : lstring Gram.entry @@ -232,7 +232,7 @@ module Constr : val binder_constr : constr_expr Gram.entry val operconstr : constr_expr Gram.entry val ident : Id.t Gram.entry - val global : reference Gram.entry + val global : qualid Gram.entry val universe_level : Glob_term.glob_level Gram.entry val sort : Glob_term.glob_sort Gram.entry val sort_family : Sorts.family Gram.entry diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 1e0589fac..4ede11b5c 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -596,19 +596,18 @@ let warns () = let rec locate_ref = function | [] -> [],[] - | r::l -> - let q = qualid_of_reference r in - let mpo = try Some (Nametab.locate_module q.CAst.v) with Not_found -> None + | qid::l -> + let mpo = try Some (Nametab.locate_module qid) with Not_found -> None and ro = - try Some (Smartlocate.global_with_alias r) + try Some (Smartlocate.global_with_alias qid) with Nametab.GlobalizationError _ | UserError _ -> None in match mpo, ro with - | None, None -> Nametab.error_global_not_found q + | None, None -> Nametab.error_global_not_found qid | 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.CAst.v,mp,r); + warning_ambiguous_name (qid,mp,r); let refs,mps = locate_ref l in refs,mp::mps (*s Recursive extraction in the Coq toplevel. The vernacular command is diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 77f1fb5ef..54fde2ca4 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -13,14 +13,14 @@ open Names open Libnames -val simple_extraction : reference -> unit -val full_extraction : string option -> reference list -> unit -val separate_extraction : reference list -> unit +val simple_extraction : qualid -> unit +val full_extraction : string option -> qualid list -> unit +val separate_extraction : qualid list -> unit val extraction_library : bool -> Id.t -> unit (* For the test-suite : extraction to a temporary file + ocamlc on it *) -val extract_and_compile : reference list -> unit +val extract_and_compile : qualid list -> unit (* For debug / external output via coqtop.byte + Drop : *) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 5bf944434..a8baeaf1b 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -194,17 +194,17 @@ val find_custom_match : ml_branch array -> string (*s Extraction commands. *) val extraction_language : lang -> unit -val extraction_inline : bool -> reference list -> unit +val extraction_inline : bool -> qualid list -> unit val print_extraction_inline : unit -> Pp.t val reset_extraction_inline : unit -> unit val extract_constant_inline : - bool -> reference -> string list -> string -> unit + bool -> qualid -> string list -> string -> unit val extract_inductive : - reference -> string -> string list -> string option -> unit + qualid -> string -> string list -> string option -> unit type int_or_id = ArgInt of int | ArgId of Id.t -val extraction_implicit : reference -> int_or_id list -> unit +val extraction_implicit : qualid -> int_or_id list -> unit (*s Table of blacklisted filenames *) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 30deb6f49..7e54bc8ad 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -17,7 +17,6 @@ open Goptions open Tacmach.New open Tacticals.New open Tacinterp -open Libnames open Stdarg open Tacarg open Pcoq.Prim @@ -127,7 +126,7 @@ let normalize_evaluables= open Genarg open Ppconstr open Printer -let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference +let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x))) let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a158fc8ff..31496513a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -627,7 +627,7 @@ let build_scheme fas = Smartlocate.global_with_alias f with Not_found -> user_err ~hdr:"FunInd.build_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) + (str "Cannot find " ++ Libnames.pr_qualid f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in @@ -668,7 +668,7 @@ let build_case_scheme fa = try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) with Not_found -> user_err ~hdr:"FunInd.build_case_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) in + (str "Cannot find " ++ Libnames.pr_qualid f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Constant.repr3 first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 33aeafef8..97f9acdb3 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -36,5 +36,5 @@ exception No_graph_found val make_scheme : Evd.evar_map ref -> (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list -val build_scheme : (Id.t*Libnames.reference*Sorts.family) list -> unit -val build_case_scheme : (Id.t*Libnames.reference*Sorts.family) -> unit +val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit +val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 9899b7b21..a2d31780d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -168,7 +168,7 @@ END let pr_fun_scheme_arg (princ_name,fun_name,s) = Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ - Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ + Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++ Termops.pr_sort_family s VERNAC ARGUMENT EXTEND fun_scheme_arg @@ -181,11 +181,11 @@ let warning_error names e = let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in warn_cannot_define_graph (names,error) | Defining_principle e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then CErrors.print e else mt () in warn_cannot_define_principle (names,error) | _ -> raise e diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index cd640eebd..489a40ed0 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -362,17 +362,17 @@ 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 = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in + let f_R_mut = qualid_of_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!") + (pr_qualid f_R_mut++str ": Not an inductive type!") locate_ind f_R_mut) in let fname_kn (((fname,_),_,_,_,_),_) = - let f_ref = CAst.map (fun n -> Ident n) fname in - locate_with_msg - (pr_reference f_ref++str ": Not an inductive type!") + let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in + locate_with_msg + (pr_qualid f_ref++str ": Not an inductive type!") locate_constant f_ref in @@ -477,7 +477,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,CAst.make @@ Ident fname,None) , + (None,qualid_of_ident fname,None) , (List.map (function | {CAst.v=Anonymous} -> assert false @@ -487,7 +487,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 (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))), + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in @@ -544,9 +544,9 @@ 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 - CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path - (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) - in + Libnames.qualid_of_path + (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")) + in let fun_from_mes = let applied_mes = Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in @@ -727,12 +727,10 @@ 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 - | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> - CAppExpl((None,r,None),new_args) - | _ -> b - end + | CRef (qid,_) as b -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((None,qid,None),new_args) + else b | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) @@ -746,13 +744,10 @@ let rec add_args id new_args = CAst.map (function add_args id new_args b1) | CLetIn(na,b1,t,b2) -> CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) - | CAppExpl((pf,r,us),exprl) -> - begin - match r with - | {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 + | CAppExpl((pf,qid,us),exprl) -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((pf,qid,us),new_args@(List.map (add_args id new_args) exprl)) + else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl) | CApp((pf,b),bl) -> CApp((pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl) @@ -888,7 +883,7 @@ let make_graph (f_ref : GlobRef.t) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None)) + CRef(Libnames.qualid_of_ident ?loc @@ 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 c6faa142a..4eee2c7a4 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -31,9 +31,7 @@ let id_of_name = function Name id -> id | _ -> raise Not_found -let locate ref = - let {CAst.v=qid} = qualid_of_reference ref in - Nametab.locate qid +let locate qid = Nametab.locate qid let locate_ind ref = match locate ref with diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 346b21ef2..7e52ee224 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -20,11 +20,11 @@ val array_get_start : 'a array -> 'a array val id_of_name : Name.t -> Id.t -val locate_ind : Libnames.reference -> inductive -val locate_constant : Libnames.reference -> Constant.t +val locate_ind : Libnames.qualid -> inductive +val locate_constant : Libnames.qualid -> Constant.t val locate_with_msg : - Pp.t -> (Libnames.reference -> 'a) -> - Libnames.reference -> 'a + Pp.t -> (Libnames.qualid -> 'a) -> + Libnames.qualid -> 'a val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list val list_union_eq : diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index aa49148fc..7298342e1 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 = CAst.make @@ Libnames.Ident na in + let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1577,7 +1577,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 [CAst.make @@ Ident term_id] in + let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_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_auto.ml4 b/plugins/ltac/g_auto.ml4 index 642e52155..35ed14fc1 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -173,7 +173,7 @@ TACTIC EXTEND convert_concl_no_check | ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ] END -let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference +let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global let glob_hints_path_atom ist = Hints.glob_hints_path_atom @@ -189,7 +189,7 @@ ARGUMENT EXTEND hints_path_atom END let pr_hints_path prc prx pry c = Hints.pp_hints_path c -let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c +let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c let glob_hints_path ist = Hints.glob_hints_path ARGUMENT EXTEND hints_path diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index d7d642e50..620f14707 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -39,11 +39,12 @@ let genarg_of_ipattern pat = in_gen (rawwit Tacarg.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 = 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.")) +let reference_to_id qid = + if Libnames.qualid_is_ident qid then + CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid + else + CErrors.user_err ?loc:qid.CAst.loc + (str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" @@ -199,8 +200,7 @@ GEXTEND Gram verbose most of the time. *) fresh_id: [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) - | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in - Locus.ArgVar (CAst.make ~loc:!@loc id) ] ] + | qid = qualid -> Locus.ArgVar (CAst.make ~loc:!@loc @@ Libnames.qualid_basename qid) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -475,7 +475,7 @@ END VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY | [ "Print" "Ltac" reference(r) ] -> - [ Feedback.msg_notice (Tacintern.print_ltac (Libnames.qualid_of_reference r).CAst.v) ] + [ Feedback.msg_notice (Tacintern.print_ltac r) ] END VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY @@ -483,7 +483,7 @@ VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY [ Tacentries.print_located_tactic r ] END -let pr_ltac_ref = Libnames.pr_reference +let pr_ltac_ref = Libnames.pr_qualid let pr_tacdef_body tacdef_body = let id, redef, body = @@ -510,8 +510,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r - | TacticRedefinition ({CAst.v=Ident r},_) -> r - | TacticRedefinition ({CAst.v=Qualid q},_) -> snd(repr_qualid q)) l), VtLater + | TacticRedefinition (qid,_) -> qualid_basename qid) 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 352e92c2a..1f56244c7 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -12,7 +12,6 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -open Libnames open Constrexpr open Constrexpr_ops open Stdarg @@ -49,7 +48,7 @@ module Tactic = Pltac open Pcoq -let sigref = mkRefC (CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Init.Specif.sig")) +let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig") type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type @@ -68,7 +67,7 @@ GEXTEND Gram Constr.closed_binder: [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in + let typ = mkAppC (sigref !@loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in [CLocalAssum ([id], default_binder_kind, typ)] ] ]; diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 2189e224f..f1634f156 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -67,13 +67,13 @@ let subst_strategy s str = str let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>" let pr_raw_strategy prc prlc _ (s : raw_strategy) = - let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_reference, prc) in + let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in Rewrite.pr_strategy prc prr s let pr_glob_strategy prc prlc _ (s : glob_strategy) = let prr = Pptactic.pr_red_expr (Ppconstr.pr_constr_expr, Ppconstr.pr_lconstr_expr, - Pputils.pr_or_by_notation Libnames.pr_reference, + Pputils.pr_or_by_notation Libnames.pr_qualid, Ppconstr.pr_constr_expr) in Rewrite.pr_strategy prc prr s diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 05005c733..31bc34a32 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -156,7 +156,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 -> - TacCase (with_evar,(clear,(CAst.make @@ CRef (CAst.make ?loc:id.CAst.loc @@ Ident id.CAst.v,None),NoBindings))) + TacCase (with_evar,(clear,(CAst.make @@ CRef (qualid_of_ident ?loc:id.CAst.loc id.CAst.v,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 4c075d413..c5aa542fd 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -21,8 +21,8 @@ val open_constr : constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry -val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry -val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry +val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry +val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index e19a95e84..09179dad3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -17,7 +17,6 @@ open Constrexpr open Genarg open Geninterp open Stdarg -open Libnames open Notation_gram open Tactypes open Locus @@ -1109,8 +1108,8 @@ let pr_goal_selector ~toplevel s = pr_lconstr = pr_lconstr_expr; pr_pattern = pr_constr_pattern_expr; pr_lpattern = pr_lconstr_pattern_expr; - pr_constant = pr_or_by_notation pr_reference; - pr_reference = pr_reference; + pr_constant = pr_or_by_notation pr_qualid; + pr_reference = pr_qualid; pr_name = pr_lident; pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg); pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; @@ -1323,7 +1322,7 @@ let () = let open Genprint in register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; register_basic_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) pr_global; + pr_qualid (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; register_basic_print0 wit_var pr_lident pr_lident pr_id; register_print0 @@ -1357,7 +1356,7 @@ let () = ; Genprint.register_print0 wit_red_expr - (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))) + (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr))) (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))) pr_red_expr_env ; diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index cd04f4ae9..01c52c413 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1773,11 +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,CAst.make @@ Libnames.Ident (Id.of_string s),None),l) +let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l) let declare_an_instance n s args = (((CAst.make @@ Name n),None), Explicit, - CAst.make @@ CAppExpl ((None, CAst.make @@ Qualid (qualid_of_string s),None), args)) + CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] @@ -1791,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 - [(CAst.make @@ Ident (Id.of_string "reflexivity"),lemma)] + [(qualid_of_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 - [(CAst.make @@ Ident (Id.of_string "symmetry"),lemma)] + [(qualid_of_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 - [(CAst.make @@ Ident (Id.of_string "transitivity"),lemma)] + [(qualid_of_ident (Id.of_string "transitivity"),lemma)] let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = init_setoid (); @@ -1825,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 - [(CAst.make @@ Ident (Id.of_string "PreOrder_Reflexive"), lemma1); - (CAst.make @@ Ident (Id.of_string "PreOrder_Transitive"),lemma3)]) + [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); + (qualid_of_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 - [(CAst.make @@ Ident (Id.of_string "PER_Symmetric"), lemma2); - (CAst.make @@ Ident (Id.of_string "PER_Transitive"),lemma3)]) + [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); + (qualid_of_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 @@ -1842,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 - [(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)]) + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]) let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) @@ -1949,16 +1949,15 @@ 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 - [(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])]) + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + (qualid_of_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 = CAst.make @@ Qualid tacpath in - TacArg (Loc.tag @@ (TacCall (Loc.tag (tacname, [])))) + let tacqid = Libnames.qualid_of_string name in + TacArg (Loc.tag @@ (TacCall (Loc.tag (tacqid, [])))) let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> @@ -2008,7 +2007,7 @@ let add_morphism glob binders m s n = let instance = (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( - (None, CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), + (None, 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 fada7424c..98d451536 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -449,12 +449,12 @@ let register_ltac local tacl = in let () = if is_shadowed then warn_unusable_identifier id in NewTac id, body - | Tacexpr.TacticRedefinition (ident, body) -> + | Tacexpr.TacticRedefinition (qid, body) -> let kn = - try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v + try Tacenv.locate_tactic qid with Not_found -> - CErrors.user_err ?loc:ident.CAst.loc - (str "There is no Ltac named " ++ pr_reference ident ++ str ".") + CErrors.user_err ?loc:qid.CAst.loc + (str "There is no Ltac named " ++ pr_qualid qid ++ str ".") in UpdateTac kn, body in diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 3f804ee8d..2bfbbe2e1 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -65,7 +65,7 @@ val create_ltac_quotation : string -> val print_ltacs : unit -> unit (** Display the list of ltac definitions currently available. *) -val print_located_tactic : Libnames.reference -> unit +val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) type _ ty_sig = diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index d51de8c65..06d2711ad 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -333,8 +333,8 @@ type glob_tactic_arg = type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation -type r_ref = reference +type r_cst = qualid or_by_notation +type r_ref = qualid type r_nam = lident type r_lev = rlevel @@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 01eead164..71e1edfd7 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -333,8 +333,8 @@ type glob_tactic_arg = type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation -type r_ref = reference +type r_cst = qualid or_by_notation +type r_ref = qualid type r_nam = lident type r_lev = rlevel @@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index cef5bb1b8..481fc30df 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -92,88 +92,83 @@ let intern_or_var f ist = function 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 - | {CAst.loc;v=Ident id} when find_var id ist -> - ArgVar (make ?loc id) - | r -> - 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 - | {loc;v=Ident id} -> - if find_var id ist then - (* A local variable of any type *) - ArgVar (make ?loc id) - else raise Not_found - | _ -> - raise Not_found - -let intern_constr_reference strict ist = function - | {v=Ident id} as r when not strict && find_hyp id ist -> - (DAst.make @@ GVar id), Some (make @@ CRef (r,None)) - | {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 - DAst.make @@ GRef (locate_global_with_alias lqid,None), - if strict then None else Some (make @@ CRef (r,None)) +let intern_global_reference ist qid = + if qualid_is_ident qid && find_var (qualid_basename qid) ist then + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + else + try ArgArg (qid.CAst.loc,locate_global_with_alias qid) + with Not_found -> error_global_not_found qid + +let intern_ltac_variable ist qid = + if qualid_is_ident qid && find_var (qualid_basename qid) ist then + (* A local variable of any type *) + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + else raise Not_found + +let intern_constr_reference strict ist qid = + let id = qualid_basename qid in + if qualid_is_ident qid && not strict && find_hyp (qualid_basename qid) ist then + (DAst.make @@ GVar id), Some (make @@ CRef (qid,None)) + else if qualid_is_ident qid && find_var (qualid_basename qid) ist then + (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (qid,None)) + else + DAst.make @@ GRef (locate_global_with_alias qid,None), + if strict then None else Some (make @@ CRef (qid,None)) (* Internalize an isolated reference in position of tactic *) -let intern_isolated_global_tactic_reference r = - let {loc;v=qid} = qualid_of_reference r in +let intern_isolated_global_tactic_reference qid = + let loc = qid.CAst.loc in TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) -let intern_isolated_tactic_reference strict ist r = +let intern_isolated_tactic_reference strict ist qid = (* An ltac reference *) - try Reference (intern_ltac_variable ist r) + try Reference (intern_ltac_variable ist qid) with Not_found -> (* A global tactic *) - try intern_isolated_global_tactic_reference r + try intern_isolated_global_tactic_reference qid with Not_found -> (* Tolerance for compatibility, allow not to use "constr:" *) - try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) + try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Reference not found *) - error_global_not_found (qualid_of_reference r) + error_global_not_found qid (* Internalize an applied tactic reference *) -let intern_applied_global_tactic_reference r = - let {loc;v=qid} = qualid_of_reference r in - ArgArg (loc,Tacenv.locate_tactic qid) +let intern_applied_global_tactic_reference qid = + ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid) -let intern_applied_tactic_reference ist r = +let intern_applied_tactic_reference ist qid = (* An ltac reference *) - try intern_ltac_variable ist r + try intern_ltac_variable ist qid with Not_found -> (* A global tactic *) - try intern_applied_global_tactic_reference r + try intern_applied_global_tactic_reference qid with Not_found -> (* Reference not found *) - error_global_not_found (qualid_of_reference r) + error_global_not_found qid (* Intern a reference parsed in a non-tactic entry *) -let intern_non_tactic_reference strict ist r = +let intern_non_tactic_reference strict ist qid = (* An ltac reference *) - try Reference (intern_ltac_variable ist r) + try Reference (intern_ltac_variable ist qid) with Not_found -> (* A constr reference *) - try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) + try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Tolerance for compatibility, allow not to use "ltac:" *) - try intern_isolated_global_tactic_reference r + try intern_isolated_global_tactic_reference qid with Not_found -> (* By convention, use IntroIdentifier for unbound ident, when not in a def *) - match r with - | {loc;v=Ident id} when not strict -> - let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in + if qualid_is_ident qid && not strict then + let id = qualid_basename qid in + let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc:qid.CAst.loc @@ IntroNaming (IntroIdentifier id)) in TacGeneric ipat - | _ -> - (* Reference not found *) - error_global_not_found (qualid_of_reference r) + else + (* Reference not found *) + error_global_not_found qid let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -269,7 +264,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 (make @@ Ident id, None)) in + let c, p = intern_constr ist (make @@ CRef (qualid_of_ident id, None)) in match DAst.get c with | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id) | _ -> clear,ElimOnConstr ((c, p), NoBindings) @@ -277,16 +272,15 @@ let intern_destruction_arg ist = function clear,ElimOnIdent (make ?loc id) let short_name = function - | {v=AN {loc;v=Ident id}} when not !strict_check -> Some (make ?loc id) + | {v=AN qid} when qualid_is_ident qid && not !strict_check -> + Some (make ?loc:qid.CAst.loc @@ qualid_basename qid) | _ -> None -let intern_evaluable_global_reference ist r = - let lqid = qualid_of_reference r in - try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true lqid) +let intern_evaluable_global_reference ist qid = + try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) with Not_found -> - match r with - | {loc;v=Ident id} when not !strict_check -> EvalVarRef id - | _ -> error_global_not_found lqid + if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) + else error_global_not_found qid let intern_evaluable_reference_or_by_notation ist = function | {v=AN r} -> intern_evaluable_global_reference ist r @@ -296,14 +290,19 @@ let intern_evaluable_reference_or_by_notation ist = function (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) (* Globalize a reduction expression *) -let intern_evaluable ist = function - | {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 - let na = short_name r in - ArgArg (e,na) +let intern_evaluable ist r = + let f ist r = + let e = intern_evaluable_reference_or_by_notation ist r in + let na = short_name r in + ArgArg (e,na) + in + match r with + | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist -> + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist -> + let id = qualid_basename qid in + ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id)) + | _ -> f ist r let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) @@ -356,7 +355,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = subterm matched when a pattern *) let r = match r with | {v=AN r} -> r - | {loc} -> make ?loc @@ Qualid (qualid_of_path (path_of_global (smart_global r))) in + | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 04dd7d6e9..9d1cc1643 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -361,7 +361,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 (make ?loc @@ qualid_of_ident id) + with Not_found -> error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -377,14 +377,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found (make ?loc @@ qualid_of_ident id) + | _ -> error_global_not_found (qualid_of_ident ?loc 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 (make ?loc @@ qualid_of_ident id) + with Not_found -> error_global_not_found (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -643,7 +643,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 (make ?loc @@ qualid_of_ident id)) + error_global_not_found (qualid_of_ident ?loc 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 @@ -925,7 +925,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 (make ?loc @@ Ident id,None))) in + let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (qualid_of_ident ?loc 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/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 5e4c9214a..e9ce306e8 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -42,11 +42,11 @@ let pr_ring_mod = function | Ring_kind Abstract -> str "abstract" | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" - | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext - | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml index 3eb68b518..a83c79d11 100644 --- a/plugins/setoid_ring/newring_ast.ml +++ b/plugins/setoid_ring/newring_ast.ml @@ -22,7 +22,7 @@ type 'constr coeff_spec = type cst_tac_spec = CstTac of raw_tactic_expr - | Closed of reference list + | Closed of qualid list type 'constr ring_mod = Ring_kind of 'constr coeff_spec diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index 3eb68b518..a83c79d11 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -22,7 +22,7 @@ type 'constr coeff_spec = type cst_tac_spec = CstTac of raw_tactic_expr - | Closed of reference list + | Closed of qualid list type 'constr ring_mod = Ring_kind of 'constr coeff_spec diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 2a31157be..54f3f9c71 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -858,7 +858,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 (CAst.make ?loc @@ Ident id, None) +let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 352f88bb3..7a1d06fdc 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1154,7 +1154,8 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar END let bvar_lname = let open CAst in function - | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id + | { v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid) | { loc = loc } -> CAst.make ?loc Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c @@ -1246,7 +1247,8 @@ END let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function - | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc (qualid_basename qid) | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 939e97866..7ce2dd64a 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -28,7 +28,6 @@ open Globnames open Stdarg open Genarg open Decl_kinds -open Libnames open Pp open Ppconstr open Printer @@ -143,21 +142,21 @@ END let declare_one_prenex_implicit locality f = let fref = try Smartlocate.global_with_alias f - with _ -> errorstrm (pr_reference f ++ str " is not declared") in + with _ -> errorstrm (pr_qualid f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args' | args' when List.exists Impargs.is_status_implicit args' -> - errorstrm (str "Expected prenex implicits for " ++ pr_reference f) + errorstrm (str "Expected prenex implicits for " ++ pr_qualid f) | _ -> [] in let impls = match Impargs.implicits_of_global fref with | [cond,impls] -> impls - | [] -> errorstrm (str "Expected some implicits for " ++ pr_reference f) + | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f) | _ -> errorstrm (str "Multiple implicits not supported") in match loop impls with | [] -> - errorstrm (str "Expected some implicits for " ++ pr_reference f) + errorstrm (str "Expected some implicits for " ++ pr_qualid f) | impls -> Impargs.declare_manual_implicits locality fref ~enriching:false [impls] @@ -415,7 +414,7 @@ let interp_search_arg arg = (* Module path postfilter *) -let pr_modloc (b, m) = if b then str "-" ++ pr_reference m else pr_reference m +let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc @@ -433,10 +432,9 @@ GEXTEND Gram END let interp_modloc mr = - let interp_mod (_, mr) = - let {CAst.loc=loc; v=qid} = qualid_of_reference mr in + let interp_mod (_, qid) = try Nametab.full_name_module qid with Not_found -> - CErrors.user_err ?loc (str "No Module " ++ pr_qualid qid) in + CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in let mr_out, mr_in = List.partition fst mr in let interp_bmod b = function | [] -> fun _ _ _ -> true diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 69d944fa1..c20e415b4 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -131,9 +131,12 @@ let add_genarg tag pr = (** Constructors for cast type *) let dC t = CastConv t (** Constructors for constr_expr *) -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 isCVar = function { CAst.v = CRef (qid,_) } -> qualid_is_ident qid | _ -> false +let destCVar = function + | { CAst.v = CRef (qid,_) } when qualid_is_ident qid -> + qualid_basename qid + | _ -> + 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) | _ -> CErrors.anomaly (str "not a GLambda") @@ -1019,8 +1022,10 @@ 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 ({CAst.v=Ident x}, _) } -> Some x - | _, Some { v = CAppExpl ((_, {CAst.v=Ident x}, _), []) } -> Some x + | _, Some { v = CRef (qid, _) } when qualid_is_ident qid -> + Some (qualid_basename qid) + | _, Some { v = CAppExpl ((_, qid, _), []) } when qualid_is_ident qid -> + Some (qualid_basename qid) | 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 df89d9eac..019ec3d27 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -87,7 +87,7 @@ let encode_tuple ({CAst.loc} as r) = module PrintingInductiveMake = functor (Test : sig - val encode : reference -> inductive + val encode : qualid -> inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 5310455fe..8695d52b1 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -87,7 +87,7 @@ val subst_genarg_hook : module PrintingInductiveMake : functor (Test : sig - val encode : Libnames.reference -> Names.inductive + val encode : Libnames.qualid -> Names.inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string @@ -95,7 +95,7 @@ module PrintingInductiveMake : sig type t = Names.inductive val compare : t -> t -> int - val encode : Libnames.reference -> Names.inductive + val encode : Libnames.qualid -> Names.inductive val subst : substitution -> t -> t val printer : t -> Pp.t val key : Goptions.option_name diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 11cfd2040..ba193da60 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -51,7 +51,7 @@ let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true | GType l1, GType l2 -> - List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2 | _ -> false let binding_kind_eq bk1 bk2 = match bk1, bk2 with diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 54fa5328f..86245d479 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -33,11 +33,11 @@ type 'a universe_kind = | UUnknown | UNamed of 'a -type level_info = Libnames.reference universe_kind +type level_info = Libnames.qualid universe_kind type glob_level = level_info glob_sort_gen type glob_constraint = glob_level * Univ.constraint_type * glob_level -type sort_info = (Libnames.reference * int) option list +type sort_info = (Libnames.qualid * int) option list type glob_sort = sort_info glob_sort_gen (** Casts *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9e024b1c2..57c4d363b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -171,38 +171,37 @@ let _ = (** Miscellaneous interpretation functions *) -let interp_known_universe_level evd r = - let qid = Libnames.qualid_of_reference r in +let interp_known_universe_level evd qid = try - match r.CAst.v with - | Libnames.Ident id -> Evd.universe_of_name evd id - | Libnames.Qualid _ -> raise Not_found + let open Libnames in + if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid + else raise Not_found with Not_found -> - let univ, k = Nametab.locate_universe qid.CAst.v in + let univ, k = Nametab.locate_universe qid in Univ.Level.make univ k -let interp_universe_level_name ~anon_rigidity evd r = - try evd, interp_known_universe_level evd r +let interp_universe_level_name ~anon_rigidity evd qid = + try evd, interp_known_universe_level evd qid with Not_found -> - match r with (* Qualified generated name *) - | {CAst.loc; v=Libnames.Qualid qid} -> - let dp, i = Libnames.repr_qualid qid in - let num = - try int_of_string (Id.to_string i) - with Failure _ -> - user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r)) - in - let level = Univ.Level.make dp num in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - | {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" - (Pp.(str "Undeclared universe: " ++ Id.print id)) + if Libnames.qualid_is_ident qid then (* Undeclared *) + let id = Libnames.qualid_basename qid in + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd + else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ Id.print id)) + else + let dp, i = Libnames.repr_qualid qid in + let num = + try int_of_string (Id.to_string i) + with Failure _ -> + user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid)) + in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with UGraph.AlreadyDeclared -> evd + in evd, level let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in @@ -232,10 +231,10 @@ let interp_known_level_info ?loc evd = function | UUnknown | UAnonymous -> user_err ?loc ~hdr:"interp_known_level_info" (str "Anonymous universes not allowed here.") - | UNamed ref -> - try interp_known_universe_level evd ref + | UNamed qid -> + try interp_known_universe_level evd qid with Not_found -> - user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) + user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid) let interp_level_info ?loc evd : level_info -> _ = function | UUnknown -> new_univ_level_variable ?loc univ_rigid evd diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 605781993..e38da45b9 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -159,7 +159,7 @@ let tag_var = tag Tag.variable let pr_univ_expr = function | Some (x,n) -> - pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) + pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) | None -> str"_" let pr_univ l = @@ -180,7 +180,7 @@ let tag_var = tag Tag.variable | GSet -> tag_type (str "Set") | GType UUnknown -> tag_type (str "Type") | GType UAnonymous -> tag_type (str "_") - | GType (UNamed u) -> tag_type (pr_reference u) + | GType (UNamed u) -> tag_type (pr_qualid u) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -205,16 +205,16 @@ let tag_var = tag Tag.variable tag_type (str "Set") | GType u -> (match u with - | UNamed u -> pr_reference u + | UNamed u -> pr_qualid u | UAnonymous -> tag_type (str "Type") | UUnknown -> tag_type (str "_")) let pr_universe_instance l = pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l - let pr_reference = CAst.with_val (function - | Qualid qid -> pr_qualid qid - | Ident id -> tag_var (pr_id id)) + let pr_reference qid = + if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid) + else pr_qualid qid let pr_cref ref us = pr_reference ref ++ pr_universe_instance us @@ -564,9 +564,9 @@ let tag_var = tag Tag.variable return (p ++ prlist (pr spc (lapp,L)) l2, lapp) else return (p, lproj) - | CAppExpl ((None,{v=Ident var},us),[t]) - | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None]) - when Id.equal var Notation_ops.ldots_var -> + | CAppExpl ((None,qid,us),[t]) + | CApp ((_, {v = CRef(qid,us)}),[t,None]) + when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var -> return ( hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index ce37c3614..bca419c9a 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -47,7 +47,7 @@ val pr_guard_annot : (constr_expr -> Pp.t) -> lident option * recursion_order_expr -> Pp.t -val pr_record_body : (reference * constr_expr) list -> Pp.t +val pr_record_body : (qualid * constr_expr) list -> Pp.t val pr_binders : local_binder_expr list -> Pp.t val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fe6cf73c7..5e5d00362 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -344,8 +344,7 @@ let register_locatable name f = exception ObjFound of logical_name -let locate_any_name ref = - let {v=qid} = qualid_of_reference ref in +let locate_any_name qid = try Term (Nametab.locate qid) with Not_found -> try Syntactic (Nametab.locate_syndef qid) @@ -452,8 +451,7 @@ type locatable_kind = | LocOther of string | LocAny -let print_located_qualid name flags ref = - let {v=qid} = qualid_of_reference ref in +let print_located_qualid name flags qid = let located = match flags with | LocTerm -> locate_term qid | LocModule -> locate_modtype qid @ locate_module qid @@ -787,10 +785,9 @@ let print_full_pure_context env sigma = follows the definition of the inductive type *) (* This is designed to print the contents of an opened section *) -let read_sec_context r = - let qid = qualid_of_reference r in +let read_sec_context qid = let dir = - try Nametab.locate_section qid.v + try Nametab.locate_section qid with Not_found -> user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in let rec get_cxt in_cxt = function diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 0375cfc92..8dd729610 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -24,20 +24,20 @@ val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node val print_full_context : env -> Evd.evar_map -> Pp.t val print_full_context_typ : env -> Evd.evar_map -> Pp.t val print_full_pure_context : env -> Evd.evar_map -> Pp.t -val print_sec_context : env -> Evd.evar_map -> reference -> Pp.t -val print_sec_context_typ : env -> Evd.evar_map -> reference -> Pp.t +val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : env -> Evd.evar_map -> reference Constrexpr.or_by_notation -> +val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t -val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t -val print_about : env -> Evd.evar_map -> reference Constrexpr.or_by_notation -> +val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t +val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t -val print_impargs : reference Constrexpr.or_by_notation -> Pp.t +val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) val print_graph : env -> evar_map -> Pp.t @@ -77,10 +77,10 @@ val register_locatable : string -> 'a locatable_info -> unit name describing the kind of objects considered and that is added as a grammar command prefix for vernacular commands Locate. *) -val print_located_qualid : reference -> Pp.t -val print_located_term : reference -> Pp.t -val print_located_module : reference -> Pp.t -val print_located_other : string -> reference -> Pp.t +val print_located_qualid : qualid -> Pp.t +val print_located_term : qualid -> Pp.t +val print_located_module : qualid -> Pp.t +val print_located_other : string -> qualid -> Pp.t type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; diff --git a/printing/printer.ml b/printing/printer.ml index 72030dc9f..d76bd1e2b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -229,15 +229,15 @@ let dirpath_of_global = function dirpath_of_mp (MutInd.modpath kn) | VarRef _ -> DirPath.empty -let qualid_of_global env r = - Libnames.make_qualid (dirpath_of_global r) (id_of_global env r) +let qualid_of_global ?loc env r = + Libnames.make_qualid ?loc (dirpath_of_global r) (id_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 vars r with e when CErrors.noncritical e -> - CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r) + qualid_of_global ?loc env r in Constrextern.set_extern_reference extern_ref; try diff --git a/stm/stm.ml b/stm/stm.ml index c394be22e..0aed88a53 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2558,8 +2558,8 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = let load_objs libs = let rq_file (dir, from, exp) = - 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 + let mp = Libnames.qualid_of_string dir in + let mfrom = Option.map Libnames.qualid_of_string 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 d49c8aaa5..85ff02824 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -125,7 +125,7 @@ type 'a hints_path_gen = | PathEmpty | PathEpsilon -type pre_hints_path = Libnames.reference hints_path_gen +type pre_hints_path = Libnames.qualid hints_path_gen type hints_path = GlobRef.t hints_path_gen type hint_term = @@ -157,7 +157,7 @@ type hint_entry = GlobRef.t option * raw_hint hint_ast with_uid with_metadata type reference_or_constr = - | HintsReference of reference + | HintsReference of qualid | HintsConstr of Constrexpr.constr_expr type hint_mode = @@ -167,12 +167,12 @@ type hint_mode = type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list - | HintsResolveIFF of bool * reference list * int option + | HintsResolveIFF of bool * qualid list * int option | HintsImmediate of reference_or_constr list - | HintsUnfold of reference list - | HintsTransparency of reference list * bool - | HintsMode of reference * hint_mode list - | HintsConstructors of reference list + | HintsUnfold of qualid list + | HintsTransparency of qualid list * bool + | HintsMode of qualid * hint_mode list + | HintsConstructors of qualid list | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument type import_level = [ `LAX | `WARN | `STRICT ] @@ -1360,7 +1360,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:qid.CAst.loc "<>" (string_of_reference qid) "ind"; + Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind"; List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in diff --git a/tactics/hints.mli b/tactics/hints.mli index e958f986e..ca18f835a 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -73,7 +73,7 @@ type search_entry type hint_entry type reference_or_constr = - | HintsReference of Libnames.reference + | HintsReference of Libnames.qualid | HintsConstr of Constrexpr.constr_expr type hint_mode = @@ -83,12 +83,12 @@ type hint_mode = type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list - | HintsResolveIFF of bool * Libnames.reference list * int option + | HintsResolveIFF of bool * Libnames.qualid list * int option | HintsImmediate of reference_or_constr list - | HintsUnfold of Libnames.reference list - | HintsTransparency of Libnames.reference list * bool - | HintsMode of Libnames.reference * hint_mode list - | HintsConstructors of Libnames.reference list + | HintsUnfold of Libnames.qualid list + | HintsTransparency of Libnames.qualid list * bool + | HintsMode of Libnames.qualid * hint_mode list + | HintsConstructors of Libnames.qualid list | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument type 'a hints_path_gen = @@ -99,7 +99,7 @@ type 'a hints_path_gen = | PathEmpty | PathEpsilon -type pre_hints_path = Libnames.reference hints_path_gen +type pre_hints_path = Libnames.qualid hints_path_gen type hints_path = GlobRef.t hints_path_gen val normalize_path : hints_path -> hints_path @@ -110,9 +110,9 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t val pp_hints_path : hints_path -> Pp.t val pp_hint_mode : hint_mode -> Pp.t val glob_hints_path_atom : - Libnames.reference hints_path_atom_gen -> GlobRef.t hints_path_atom_gen + Libnames.qualid hints_path_atom_gen -> GlobRef.t hints_path_atom_gen val glob_hints_path : - Libnames.reference hints_path_gen -> GlobRef.t hints_path_gen + Libnames.qualid hints_path_gen -> GlobRef.t hints_path_gen module Hint_db : sig diff --git a/vernac/classes.ml b/vernac/classes.ml index 8cf3895fb..382d18b09 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -229,10 +229,7 @@ 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 = CAst.map (function - | Ident id' -> id' - | Qualid id' -> snd (repr_qualid id')) - in + let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in let props, rest = List.fold_left (fun (props, rest) decl -> diff --git a/vernac/classes.mli b/vernac/classes.mli index eea2a211d..bd30b2d60 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -22,7 +22,7 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a (** Instance declaration *) -val existing_instance : bool -> reference -> Hints.hint_info_expr option -> unit +val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) val declare_instance_constant : diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index b93e8d9ac..6057c05f5 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -44,8 +44,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(make ?loc @@ Ident id,None))) params in - CAppExpl ((None,CAst.make ?loc @@ Ident name,None),List.rev args) + let args = List.map (fun id -> CAst.(make ?loc @@ CRef(qualid_of_ident ?loc id,None))) params in + CAppExpl ((None,qualid_of_ident ?loc name,None),List.rev args) | c -> c ) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index a6d7fccf3..eef7afbfb 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 = CAst.make @@ Qualid (qualid_of_string s) +let make_qref s = qualid_of_string s let lt_ref = make_qref "Init.Peano.lt" let rec telescope sigma l = diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 434e836d8..cc9be7b0e 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -229,7 +229,7 @@ type prod_info = production_level * production_position type (_, _) entry = | TTName : ('self, lname) entry -| TTReference : ('self, reference) entry +| TTReference : ('self, qualid) entry | TTBigint : ('self, Constrexpr.raw_natural_number) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry @@ -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 (CAst.make ?loc @@ Ident id)) + | Name id -> CPatAtom (Some (qualid_of_ident ?loc id)) type 'r env = { constrs : 'r list; diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index 3a59242de..16934fc86 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -549,7 +549,7 @@ GEXTEND Gram ] ] ; module_expr_atom: - [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ] + [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid | "("; me = module_expr; ")" -> me ] ] ; with_declaration: [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr -> @@ -559,7 +559,7 @@ GEXTEND Gram ] ] ; module_type: - [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) + [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid | "("; mt = module_type; ")" -> mt | mty = module_type; me = module_expr_atom -> CAst.make ~loc:!@loc @@ CMapply (mty,me) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 8f64f5519..da14358ef 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1449,7 +1449,7 @@ let add_notation_extra_printing_rule df k v = (* Infix notations *) -let inject_var x = CAst.make @@ CRef (CAst.make @@ Ident (Id.of_string x),None) +let inject_var x = CAst.make @@ CRef (qualid_of_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/ppvernac.ml b/vernac/ppvernac.ml index d0c423650..56dfaa54a 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -16,7 +16,6 @@ open Util open CAst open Extend -open Libnames open Decl_kinds open Constrexpr open Constrexpr_ops @@ -79,13 +78,13 @@ open Pputils let pr_lname_decl (n, u) = pr_lname n ++ pr_universe_decl u - let pr_smart_global = Pputils.pr_or_by_notation pr_reference + let pr_smart_global = Pputils.pr_or_by_notation pr_qualid - let pr_ltac_ref = Libnames.pr_reference + let pr_ltac_ref = Libnames.pr_qualid - let pr_module = Libnames.pr_reference + let pr_module = Libnames.pr_qualid - let pr_import_module = Libnames.pr_reference + let pr_import_module = Libnames.pr_qualid let sep_end = function | VernacBullet _ @@ -157,7 +156,7 @@ open Pputils let pr_locality local = if local then keyword "Local" else keyword "Global" let pr_option_ref_value = function - | QualidRefValue id -> pr_reference id + | QualidRefValue id -> pr_qualid id | StringRefValue s -> qs s let pr_printoption table b = @@ -180,7 +179,7 @@ open Pputils | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z let pr_reference_or_constr pr_c = function - | HintsReference r -> pr_reference r + | HintsReference r -> pr_qualid r | HintsConstr c -> pr_c c let pr_hint_mode = function @@ -202,24 +201,24 @@ open Pputils l | HintsResolveIFF (l2r, l, n) -> keyword "Resolve " ++ str (if l2r then "->" else "<-") - ++ prlist_with_sep sep pr_reference l + ++ prlist_with_sep sep pr_qualid l | HintsImmediate l -> keyword "Immediate" ++ spc() ++ prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l | HintsUnfold l -> - keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_reference l + keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_qualid l | HintsTransparency (l, b) -> keyword (if b then "Transparent" else "Opaque") ++ spc () - ++ prlist_with_sep sep pr_reference l + ++ prlist_with_sep sep pr_qualid l | HintsMode (m, l) -> keyword "Mode" ++ spc () - ++ pr_reference m ++ spc() ++ + ++ pr_qualid m ++ spc() ++ prlist_with_sep spc pr_hint_mode l | HintsConstructors c -> keyword "Constructors" - ++ spc() ++ prlist_with_sep spc pr_reference c + ++ spc() ++ prlist_with_sep spc pr_qualid c | HintsExtern (n,c,tac) -> let pat = match c with None -> mt () | Some pat -> pr_pat pat in keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ @@ -233,7 +232,7 @@ open Pputils keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p | CWith_Module (id,qid) -> keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ - pr_ast pr_qualid qid + pr_qualid qid let rec pr_module_ast leading_space pr_c = function | { loc ; v = CMident qid } -> @@ -451,7 +450,7 @@ open Pputils | PrintFullContext -> keyword "Print All" | PrintSectionContext s -> - keyword "Print Section" ++ spc() ++ Libnames.pr_reference s + keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s | PrintGrammar ent -> keyword "Print Grammar" ++ spc() ++ str ent | PrintLoadPath dir -> @@ -499,9 +498,9 @@ open Pputils | PrintName (qid,udecl) -> keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl | PrintModuleType qid -> - keyword "Print Module Type" ++ spc() ++ pr_reference qid + keyword "Print Module Type" ++ spc() ++ pr_qualid qid | PrintModule qid -> - keyword "Print Module" ++ spc() ++ pr_reference qid + keyword "Print Module" ++ spc() ++ pr_qualid qid | PrintInspect n -> keyword "Inspect" ++ spc() ++ int n | PrintScopes -> @@ -604,7 +603,7 @@ open Pputils | ShowUniverses -> keyword "Show Universes" | ShowProofNames -> keyword "Show Conjectures" | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") - | ShowMatch id -> keyword "Show Match " ++ pr_reference id + | ShowMatch id -> keyword "Show Match " ++ pr_qualid id in return (pr_showable s) | VernacCheckGuard -> @@ -901,7 +900,7 @@ open Pputils | VernacDeclareInstances insts -> let pr_inst (id, info) = - pr_reference id ++ pr_hint_info pr_constr_pattern_expr info + pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info in return ( hov 1 (keyword "Existing" ++ spc () ++ @@ -911,7 +910,7 @@ open Pputils | VernacDeclareClass id -> return ( - hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id) + hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id) ) (* Modules and Module Types *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 94eb45fd3..479482095 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -183,29 +183,27 @@ let print_modules () = pr_vertical_list DirPath.print only_loaded -let print_module r = - let qid = qualid_of_reference r in +let print_module qid = try - let globdir = Nametab.locate_dir qid.v in + let globdir = Nametab.locate_dir qid 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.v) + Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) -let print_modtype r = - let qid = qualid_of_reference r in +let print_modtype qid = try - let kn = Nametab.locate_modtype qid.v in + let kn = Nametab.locate_modtype qid 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.v in + let mp = Nametab.locate_module qid in Printmod.print_module false mp with Not_found -> - user_err (str"Unknown Module Type or Module " ++ pr_qualid qid.v) + user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) let print_namespace ns = let ns = List.rev (Names.DirPath.repr ns) in @@ -367,33 +365,32 @@ let msg_found_library = function | Library.LibInPath, fulldir, file -> hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file) -let err_unmapped_library ?loc ?from qid = +let err_unmapped_library ?from qid = let dir = fst (repr_qualid qid) in let prefix = match from with | None -> str "." | Some from -> str " and prefix " ++ DirPath.print from ++ str "." in - user_err ?loc + user_err ?loc:qid.CAst.loc ~hdr:"locate_library" (strbrk "Cannot find a physical path bound to logical path matching suffix " ++ DirPath.print dir ++ prefix) -let err_notfound_library ?loc ?from qid = +let err_notfound_library ?from qid = let prefix = match from with | None -> str "." | Some from -> str " with prefix " ++ DirPath.print from ++ str "." in - user_err ?loc ~hdr:"locate_library" + user_err ?loc:qid.CAst.loc ~hdr:"locate_library" (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) -let print_located_library r = - let {loc;v=qid} = qualid_of_reference r in +let print_located_library qid = try msg_found_library (Library.locate_qualified_library ~warn:false qid) with - | Library.LibUnmappedDir -> err_unmapped_library ?loc qid - | Library.LibNotFound -> err_notfound_library ?loc qid + | Library.LibUnmappedDir -> err_unmapped_library qid + | Library.LibNotFound -> err_notfound_library qid let smart_global r = let gr = Smartlocate.smart_global r in @@ -636,7 +633,7 @@ let vernac_scheme l = let vernac_combined_scheme lid l = if Dumpglob.dump () then (Dumpglob.dump_definition lid false "def"; - List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (make ?loc @@ Ident id))) l); + List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (qualid_of_ident ?loc id))) l); Indschemes.do_combined_scheme lid l let vernac_universe ~atts l = @@ -657,7 +654,7 @@ let vernac_constraint ~atts l = (* Modules *) let vernac_import export refl = - Library.import_module export (List.map qualid_of_reference refl) + Library.import_module export refl let vernac_declare_module export {loc;v=id} binders_ast mty_ast = (* We check the state of the system (in section, in module type) @@ -675,7 +672,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 [make @@ Ident id]) export + Option.iter (fun export -> vernac_import export [qualid_of_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) @@ -700,7 +697,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 [make @@ Ident id]) export + (fun export -> vernac_import export [qualid_of_ident id]) export ) argsexport | _::_ -> let binders_ast = List.map @@ -715,14 +712,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 [make @@ Ident id]) + Option.iter (fun export -> vernac_import export [qualid_of_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 [make ?loc @@ Ident id]) export + Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then @@ -747,7 +744,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 [make ?loc @@ Ident id]) export + (fun export -> vernac_import export [qualid_of_ident ?loc id]) export ) argsexport | _ :: _ -> @@ -809,22 +806,20 @@ let warn_require_in_section = let vernac_require from import qidl = if Lib.sections_are_opened () then warn_require_in_section (); - let qidl = List.map qualid_of_reference qidl in let root = match from with | None -> None | Some from -> - let qid = Libnames.qualid_of_reference from in - let (hd, tl) = Libnames.repr_qualid qid.v in + let (hd, tl) = Libnames.repr_qualid from in Some (Libnames.add_dirpath_suffix hd tl) in - let locate {loc;v=qid} = + let locate qid = try let warn = not !Flags.quiet in let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in (dir, f) with - | Library.LibUnmappedDir -> err_unmapped_library ?loc ?from:root qid - | Library.LibNotFound -> err_notfound_library ?loc ?from:root qid + | Library.LibUnmappedDir -> err_unmapped_library ?from:root qid + | Library.LibNotFound -> err_notfound_library ?from:root qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then @@ -1687,10 +1682,10 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = let glnumopt = query_command_selector ?loc glopt in let gl,id = 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 {v=Ident id} -> (* goal number given, catch if wong *) - (try get_nth_goal n,id + | None,AN qid when qualid_is_ident qid -> (* goal number not given, catch any failure *) + (try get_nth_goal 1, qualid_basename qid with _ -> raise NoHyp) + | Some n,AN qid when qualid_is_ident qid -> (* goal number given, catch if wong *) + (try get_nth_goal n, qualid_basename qid with Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs" (str "No such goal: " ++ int n ++ str ".")) @@ -1771,11 +1766,10 @@ let vernac_print ~atts env sigma = Printer.pr_assumptionset env sigma nassums | PrintStrategy r -> print_strategy r -let global_module r = - let {loc;v=qid} = qualid_of_reference r in +let global_module qid = try Nametab.full_name_module qid with Not_found -> - user_err ?loc ~hdr:"global_module" + user_err ?loc:qid.CAst.loc ~hdr:"global_module" (str "Module/section " ++ pr_qualid qid ++ str " not found.") let interp_search_restriction = function diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 3c88a3443..02a3b2bd6 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -8,11 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit +val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit (** Vernacular entries *) val vernac_require : - Libnames.reference option -> bool option -> Libnames.reference list -> unit + Libnames.qualid option -> bool option -> Libnames.qualid list -> unit (** The main interpretation function of vernacular expressions *) val interp : diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 5acac9e25..f74383b02 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -13,7 +13,7 @@ open Constrexpr open Libnames (** Vernac expressions, produced by the parser *) -type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation +type class_rawexpr = FunClass | SortClass | RefClass of qualid or_by_notation type goal_selector = Goal_select.t = | SelectAlreadyFocused @@ -37,37 +37,37 @@ type univ_name_list = UnivNames.univ_name_list type printable = | PrintTables | PrintFullContext - | PrintSectionContext of reference + | PrintSectionContext of qualid | PrintInspect of int | PrintGrammar of string | PrintLoadPath of DirPath.t option | PrintModules - | PrintModule of reference - | PrintModuleType of reference + | PrintModule of qualid + | PrintModuleType of qualid | PrintNamespace of DirPath.t | PrintMLLoadPath | PrintMLModules | PrintDebugGC - | PrintName of reference or_by_notation * UnivNames.univ_name_list option + | PrintName of qualid or_by_notation * UnivNames.univ_name_list option | PrintGraph | PrintClasses | PrintTypeClasses - | PrintInstances of reference or_by_notation + | PrintInstances of qualid or_by_notation | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions | PrintUniverses of bool * string option - | PrintHint of reference or_by_notation + | PrintHint of qualid or_by_notation | PrintHintGoal | PrintHintDbName of string | PrintHintDb | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option - | PrintImplicit of reference or_by_notation - | PrintAssumptions of bool * bool * reference or_by_notation - | PrintStrategy of reference or_by_notation option + | PrintAbout of qualid or_by_notation * UnivNames.univ_name_list option * Goal_select.t option + | PrintImplicit of qualid or_by_notation + | PrintAssumptions of bool * bool * qualid or_by_notation + | PrintStrategy of qualid or_by_notation option type search_about_item = | SearchSubPattern of constr_pattern_expr @@ -80,11 +80,11 @@ type searchable = | SearchAbout of (bool * search_about_item) list type locatable = - | LocateAny of reference or_by_notation - | LocateTerm of reference or_by_notation - | LocateLibrary of reference - | LocateModule of reference - | LocateOther of string * reference + | LocateAny of qualid or_by_notation + | LocateTerm of qualid or_by_notation + | LocateLibrary of qualid + | LocateModule of qualid + | LocateOther of string * qualid | LocateFile of string type showable = @@ -95,7 +95,7 @@ type showable = | ShowUniverses | ShowProofNames | ShowIntros of bool - | ShowMatch of reference + | ShowMatch of qualid type comment = | CommentConstr of constr_expr @@ -103,7 +103,7 @@ type comment = | CommentInt of int type reference_or_constr = Hints.reference_or_constr = - | HintsReference of reference + | HintsReference of qualid | HintsConstr of constr_expr [@@ocaml.deprecated "Please use [Hints.reference_or_constr]"] @@ -123,18 +123,18 @@ type hint_info_expr = Hints.hint_info_expr type hints_expr = Hints.hints_expr = | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list - | HintsResolveIFF of bool * reference list * int option + | HintsResolveIFF of bool * qualid list * int option | HintsImmediate of Hints.reference_or_constr list - | HintsUnfold of reference list - | HintsTransparency of reference list * bool - | HintsMode of reference * Hints.hint_mode list - | HintsConstructors of reference list + | HintsUnfold of qualid list + | HintsTransparency of qualid list * bool + | HintsMode of qualid * Hints.hint_mode list + | HintsConstructors of qualid list | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument [@@ocaml.deprecated "Please use [Hints.hints_expr]"] type search_restriction = - | SearchInside of reference list - | SearchOutside of reference list + | SearchInside of qualid list + | SearchOutside of qualid list type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) @@ -159,7 +159,7 @@ type option_value = Goptions.option_value = type option_ref_value = | StringRefValue of string - | QualidRefValue of reference + | QualidRefValue of qualid (** Identifier and optional list of bound universes and constraints. *) @@ -222,9 +222,9 @@ type proof_end = | Proved of Proof_global.opacity_flag * lident option type scheme = - | InductionScheme of bool * reference or_by_notation * sort_expr - | CaseScheme of bool * reference or_by_notation * sort_expr - | EqualityScheme of reference or_by_notation + | InductionScheme of bool * qualid or_by_notation * sort_expr + | CaseScheme of bool * qualid or_by_notation * sort_expr + | EqualityScheme of qualid or_by_notation type section_subset_expr = | SsEmpty @@ -348,10 +348,10 @@ type nonrec vernac_expr = | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of - reference option * export_flag option * reference list - | VernacImport of export_flag * reference list - | VernacCanonical of reference or_by_notation - | VernacCoercion of reference or_by_notation * + qualid option * export_flag option * qualid list + | VernacImport of export_flag * qualid list + | VernacCanonical of qualid or_by_notation + | VernacCoercion of qualid or_by_notation * class_rawexpr * class_rawexpr | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr | VernacNameSectionHypSet of lident * section_subset_expr @@ -367,9 +367,9 @@ type nonrec vernac_expr = | VernacContext of local_binder_expr list | VernacDeclareInstances of - (reference * Hints.hint_info_expr) list (* instances names, priorities and patterns *) + (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *) - | VernacDeclareClass of reference (* inductive or definition name *) + | VernacDeclareClass of qualid (* inductive or definition name *) (* Modules and Module Types *) | VernacDeclareModule of bool option * lident * @@ -403,11 +403,11 @@ type nonrec vernac_expr = (* Commands *) | VernacCreateHintDb of string * bool - | VernacRemoveHints of string list * reference list + | VernacRemoveHints of string list * qualid list | VernacHints of string list * Hints.hints_expr | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * onlyparsing_flag - | VernacArguments of reference or_by_notation * + | VernacArguments of qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * int option (* Number of args to trigger reduction *) * @@ -416,9 +416,9 @@ type nonrec vernac_expr = `DefaultImplicits ] list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option - | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) + | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list) | VernacSetStrategy of - (Conv_oracle.level * reference or_by_notation list) list + (Conv_oracle.level * qualid or_by_notation list) list | VernacUnsetOption of export_flag * Goptions.option_name | VernacSetOption of export_flag * Goptions.option_name * option_value | VernacAddOption of Goptions.option_name * option_ref_value list |