diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-06-19 16:48:12 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-06-19 16:48:12 +0200 |
commit | 6715e6801c1d285a12eeca55dd8b831d7efb8c0d (patch) | |
tree | 2b8925708d85f7cef5fb222d551cf809704f8ebd | |
parent | c37881f3d64a6db0d7414eb18adfa4de6b64d4b1 (diff) | |
parent | 133ac4fbb9a8b4213cb3f8ca2f7c2568931209ce (diff) |
Merge PR #7797: Remove reference name type.
94 files changed, 656 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/ci/user-overlays/07797-rm-reference.sh b/dev/ci/user-overlays/07797-rm-reference.sh new file mode 100644 index 000000000..f7811cd6f --- /dev/null +++ b/dev/ci/user-overlays/07797-rm-reference.sh @@ -0,0 +1,20 @@ +_OVERLAY_BRANCH=rm-reference + +if [ "$CI_PULL_REQUEST" = "7797" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then + + Equations_CI_BRANCH="$_OVERLAY_BRANCH" + Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations.git + + ltac2_CI_BRANCH="fix-7797" + ltac2_CI_GITURL=https://github.com/ppedrot/Ltac2.git + + quickchick_CI_BRANCH="$_OVERLAY_BRANCH" + quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick.git + + coq_dpdgraph_CI_BRANCH="$_OVERLAY_BRANCH" + coq_dpdgraph_CI_GITURL=https://github.com/maximedenes/coq-dpdgraph.git + + Elpi_CI_BRANCH="$_OVERLAY_BRANCH" + Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi.git + +fi 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 5a54c6f05..fe49d64c7 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 |