diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 22:50:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 15:59:10 +0200 |
| commit | c51fb2fae0e196012de47203b8a71c61720d6c5c (patch) | |
| tree | e49c2d38b6c841dc6514944750d21ed08ab94bce | |
| parent | 437063a0c745094c5693d1c5abba46ce375d69c6 (diff) | |
[api] Deprecate GlobRef constructors.
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
90 files changed, 493 insertions, 517 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 8343853af5..aa28bce018 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -15,7 +15,6 @@ open Util open Pp open Names open Libnames -open Globnames open Univ open Environ open Printer @@ -141,7 +140,7 @@ let ppclosedglobconstridmap x = pp (pr_closed_glob_constr_idmap x) let pP s = pp (hov 0 s) -let safe_pr_global = function +let safe_pr_global = let open GlobRef in function | ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")") | IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++ int i ++ str ")") @@ -558,7 +557,7 @@ let encode_path ?loc prefix mpdir suffix id = make_qualid ?loc (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id -let raw_string_of_ref ?loc _ = function +let raw_string_of_ref ?loc _ = let open GlobRef in function | ConstRef cst -> let (mp,id) = Constant.repr2 cst in encode_path ?loc "CST" (Some mp) [] (Label.to_id id) @@ -574,7 +573,7 @@ let raw_string_of_ref ?loc _ = function | VarRef id -> encode_path ?loc "SECVAR" None [] id -let short_string_of_ref ?loc _ = function +let short_string_of_ref ?loc _ = let open GlobRef in function | VarRef id -> qualid_of_ident ?loc id | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (Constant.label cst)) | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (MutInd.label kn)) diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml index ba989b1bac..88afec14d5 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -2,14 +2,15 @@ type constr is given in the coq-dpdgraph plugin. *) let simple_body_access gref = + let open Names.GlobRef in match gref with - | Globnames.VarRef _ -> + | VarRef _ -> failwith "variables are not covered in this example" - | Globnames.IndRef _ -> + | IndRef _ -> failwith "inductive types are not covered in this example" - | Globnames.ConstructRef _ -> + | ConstructRef _ -> failwith "constructors are not covered in this example" - | Globnames.ConstRef cst -> + | ConstRef cst -> let cb = Environ.lookup_constant cst (Global.env()) in match Global.body_of_constant_body Library.indirect_accessor cb with | Some(e, _, _) -> EConstr.of_constr e diff --git a/engine/namegen.ml b/engine/namegen.ml index 77d45ce1e4..89c2fade62 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -24,7 +24,6 @@ open EConstr open Vars open Nameops open Libnames -open Globnames open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -72,7 +71,7 @@ let is_imported_modpath = function in find_prefix (Lib.current_mp ()) | _ -> false -let is_imported_ref = function +let is_imported_ref = let open GlobRef in function | VarRef _ -> false | IndRef (kn,_) | ConstructRef ((kn,_),_) -> @@ -90,7 +89,7 @@ let is_global id = let is_constructor id = try match Nametab.locate (qualid_of_ident id) with - | ConstructRef _ -> true + | GlobRef.ConstructRef _ -> true | _ -> false with Not_found -> false @@ -102,7 +101,7 @@ let is_section_variable id = (**********************************************************************) (* Generating "intuitive" names from its type *) -let global_of_constr = function +let global_of_constr = let open GlobRef in function | Const (c, _) -> ConstRef c | Ind (i, _) -> IndRef i | Construct (c, _) -> ConstructRef c @@ -149,8 +148,8 @@ let hdchar env sigma c = | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn))) | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn)) - | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") - | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.IndRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") | Var id -> lowercase_first_char id | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> diff --git a/engine/termops.ml b/engine/termops.ml index 1ed2d93b3c..2ab2f60421 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1058,7 +1058,7 @@ let is_section_variable id = with Not_found -> false let global_of_constr sigma c = - let open Globnames in + let open GlobRef in match EConstr.kind sigma c with | Const (c, u) -> ConstRef c, u | Ind (i, u) -> IndRef i, u @@ -1067,7 +1067,7 @@ let global_of_constr sigma c = | _ -> raise Not_found let is_global sigma c t = - let open Globnames in + let open GlobRef in match c, EConstr.kind sigma t with | ConstRef c, Const (c', _) -> Constant.equal c c' | IndRef i, Ind (i', _) -> eq_ind i i' @@ -1379,7 +1379,7 @@ let dependency_closure env sigma sign hyps = List.rev lh let global_app_of_constr sigma c = - let open Globnames in + let open GlobRef in match EConstr.kind sigma c with | Const (c, u) -> (ConstRef c, u), None | Ind (i, u) -> (IndRef i, u), None diff --git a/engine/univGen.ml b/engine/univGen.ml index a347bba188..b1ed3b2694 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -56,15 +56,15 @@ let fresh_global_instance ?loc ?names env gr = u, ctx let fresh_constant_instance env c = - let u, ctx = fresh_global_instance env (ConstRef c) in + let u, ctx = fresh_global_instance env (GlobRef.ConstRef c) in (c, u), ctx let fresh_inductive_instance env ind = - let u, ctx = fresh_global_instance env (IndRef ind) in + let u, ctx = fresh_global_instance env (GlobRef.IndRef ind) in (ind, u), ctx let fresh_constructor_instance env c = - let u, ctx = fresh_global_instance env (ConstructRef c) in + let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in (c, u), ctx let fresh_global_instance ?loc ?names env gr = @@ -84,10 +84,10 @@ let fresh_global_or_constr_instance env = function let global_of_constr c = match kind c with - | Const (c, u) -> ConstRef c, u - | Ind (i, u) -> IndRef i, u - | Construct (c, u) -> ConstructRef c, u - | Var id -> VarRef id, Instance.empty + | Const (c, u) -> GlobRef.ConstRef c, u + | Ind (i, u) -> GlobRef.IndRef i, u + | Construct (c, u) -> GlobRef.ConstructRef c, u + | Var id -> GlobRef.VarRef id, Instance.empty | _ -> raise Not_found let fresh_sort_in_family = function diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8573dccdf9..c8ea4d6248 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -16,7 +16,6 @@ open Names open Nameops open Termops open Libnames -open Globnames open Namegen open Impargs open CAst @@ -361,7 +360,7 @@ let mkPat ?loc qid l = CAst.make ?loc @@ if List.is_empty l then CPatAtom (Some qid) else CPatCstr (qid,None,l) let pattern_printable_in_both_syntax (ind,_ as c) = - let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in + let impl_st = extract_impargs_data (implicits_of_global (GlobRef.ConstructRef c)) in let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in List.exists (fun (_,impls) -> (List.length impls >= nb_params) && @@ -416,7 +415,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = (* we don't want to have 'x := _' in our patterns *) acc | Some c, _ -> - ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc) + ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc) | _ -> raise No_match in ip q tail acc | _ -> assert false @@ -424,14 +423,14 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = CPatRecord(List.rev (ip projs args [])) with Not_found | No_match | Exit -> - let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in + let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in if Constrintern.get_asymmetric_patterns () then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) else let full_args = add_patt_for_params (fst cstrsp) args in - match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with + match drop_implicits_in_patt (GlobRef.ConstructRef cstrsp) 0 full_args with | Some true_args -> CPatCstr (c, None, true_args) | None -> CPatCstr (c, Some full_args, []) in @@ -500,7 +499,7 @@ and extern_notation_pattern allscopes vars t = function match DAst.get t with | PatCstr (cstr,args,na) -> let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in - let p = apply_notation_to_pattern ?loc (ConstructRef cstr) + let p = apply_notation_to_pattern ?loc (GlobRef.ConstructRef cstr) (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None @@ -513,7 +512,7 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function | (keyrule,pat,n as _rule)::rules -> try if is_inactive_rule keyrule then raise No_match; - apply_notation_to_pattern (IndRef ind) + apply_notation_to_pattern (GlobRef.IndRef ind) (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with No_match -> extern_notation_ind_pattern allscopes vars ind args rules @@ -522,7 +521,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and not explicit application. *) if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then - let c = extern_reference vars (IndRef ind) in + let c = extern_reference vars (GlobRef.IndRef ind) in let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), []) else @@ -531,9 +530,9 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = extern_notation_ind_pattern allscopes vars ind args (uninterp_ind_pattern_notations ind) with No_match -> - let c = extern_reference vars (IndRef ind) in + let c = extern_reference vars (GlobRef.IndRef ind) in let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in - match drop_implicits_in_patt (IndRef ind) 0 args with + match drop_implicits_in_patt (GlobRef.IndRef ind) 0 args with |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args) |None -> CAst.make @@ CPatCstr (c, Some args, []) @@ -825,7 +824,7 @@ let rec extern inctx scopes vars r = begin try if !Flags.raw_print then raise Exit; - let cstrsp = match ref with ConstructRef c -> c | _ -> raise Not_found in + let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in let struc = Recordops.lookup_structure (fst cstrsp) in if PrintingRecord.active (fst cstrsp) then () @@ -858,7 +857,7 @@ let rec extern inctx scopes vars r = (* we give up since the constructor is not complete *) | (arg, scopes) :: tail -> let head = extern true scopes vars arg in - ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) + ip q locs' tail ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), head) :: acc) in CRecord (List.rev (ip projs locals args [])) with @@ -1238,7 +1237,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with GVar id | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None) | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) - | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None), + | PProj (p,c) -> GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p),None), [glob_of_pat avoid env sigma c]) | PApp (f,args) -> GApp (glob_of_pat avoid env sigma f,Array.map_to_list (glob_of_pat avoid env sigma) args) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 68ade75815..f341071728 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -647,7 +647,7 @@ let terms_of_binders bl = | PatVar (Name id) -> CRef (qualid_of_ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in + let qid = qualid_of_path ?loc (Nametab.path_of_global (GlobRef.ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in @@ -951,7 +951,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) - let ref = VarRef id in + let ref = GlobRef.VarRef id in let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *) @@ -1014,7 +1014,7 @@ let glob_sort_of_level (level: glob_level) : glob_sort = let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in match intern_extended_global_of_qualid qid with - | TrueGlobal (VarRef _) when no_secvar -> + | TrueGlobal (GlobRef.VarRef _) when no_secvar -> (* Rule out section vars since these should have been found by intern_var *) raise Not_found | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), Some ref, args @@ -1063,6 +1063,7 @@ let check_applied_projection isproj realref qid = match isproj with | None -> () | Some projargs -> + let open GlobRef in let is_prim = match realref with | None | Some (IndRef _ | ConstructRef _ | VarRef _) -> false | Some (ConstRef c) -> @@ -1219,7 +1220,9 @@ let insert_local_defs_in_pattern (ind,j) l = | _ -> assert false in aux decls l -let add_local_defs_and_check_length loc env g pl args = match g with +let add_local_defs_and_check_length loc env g pl args = + let open GlobRef in + match g with | ConstructRef cstr -> (* We consider that no variables corresponding to local binders have been given in the "explicit" arguments, which come from a @@ -1259,14 +1262,14 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 let add_implicits_check_constructor_length env loc c len_pl1 pl2 = let nargs = Inductiveops.constructor_nallargs env c in let nargs' = Inductiveops.constructor_nalldecls env c in - let impls_st = implicits_of_global (ConstructRef c) in + let impls_st = implicits_of_global (GlobRef.ConstructRef c) in add_implicits_check_length (error_wrong_numarg_constructor ?loc env c) nargs nargs' impls_st len_pl1 pl2 let add_implicits_check_ind_length env loc c len_pl1 pl2 = let nallargs = inductive_nallargs env c in let nalldecls = inductive_nalldecls env c in - let impls_st = implicits_of_global (IndRef c) in + let impls_st = implicits_of_global (GlobRef.IndRef c) in add_implicits_check_length (error_wrong_numarg_inductive ?loc env c) nallargs nalldecls impls_st len_pl1 pl2 @@ -1283,6 +1286,7 @@ let chop_params_pattern loc ind args with_letin = args let find_constructor loc add_params ref = + let open GlobRef in let (ind,_ as cstr) = match ref with | ConstructRef cstr -> cstr | IndRef _ -> @@ -1317,7 +1321,7 @@ let check_duplicate ?loc fields = pr_qualid r ++ str ".") let inductive_of_record loc record = - let inductive = IndRef (inductive_of_constructor record.Recordops.s_CONST) in + let inductive = GlobRef.IndRef (inductive_of_constructor record.Recordops.s_CONST) in Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive (** [sort_fields ~complete loc fields completer] expects a list @@ -1348,7 +1352,7 @@ let sort_fields ~complete loc fields completer = 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 + let global_record_id = GlobRef.ConstructRef record.Recordops.s_CONST in try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in @@ -1363,7 +1367,7 @@ let sort_fields ~complete loc fields completer = match projs with | [] -> (idx, acc_first_idx, acc) | (Some field_glob_id) :: projs -> - let field_glob_ref = ConstRef field_glob_id in + let field_glob_ref = GlobRef.ConstRef field_glob_id in let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in begin match proj_kinds with | [] -> anomaly (Pp.str "Number of projections mismatch.") @@ -1407,7 +1411,7 @@ let sort_fields ~complete loc fields completer = raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref))) in let remaining_projs, (field_index, _) = - let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in + let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (GlobRef.ConstRef glob_id) in try CList.extract_first the_proj remaining_projs with Not_found -> let ind1 = inductive_of_record loc record in @@ -1518,12 +1522,12 @@ let drop_notations_pattern looked_for genv = let ensure_kind top loc g = try if top then looked_for g else - match g with ConstructRef _ -> () | _ -> raise Not_found + match g with GlobRef.ConstructRef _ -> () | _ -> raise Not_found with Not_found -> error_invalid_pattern_notation ?loc () in let test_kind top = - if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found + if top then looked_for else function GlobRef.ConstructRef _ -> () | _ -> raise Not_found in (* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) let rec rcp_of_glob scopes x = DAst.(map (function @@ -1736,7 +1740,7 @@ let rec intern_pat genv ntnvars aliases pat = let intern_cases_pattern genv ntnvars scopes aliases pat = intern_pat genv ntnvars aliases - (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat) + (drop_notations_pattern (function GlobRef.ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat) let _ = intern_cases_pattern_fwd := @@ -1745,13 +1749,13 @@ let _ = let intern_ind_pattern genv ntnvars scopes pat = let no_not = try - drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat + drop_notations_pattern (function (GlobRef.IndRef _ | GlobRef.ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc in let loc = no_not.CAst.loc in match DAst.get no_not with | RCPatCstr (head, expl_pl, pl) -> - let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in + let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in let with_letin, pl2 = add_implicits_check_ind_length genv loc c (List.length expl_pl) pl in let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in @@ -1790,7 +1794,7 @@ let set_hole_implicit i b c = Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") end - | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),IntroAnonymous,None) + | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (GlobRef.VarRef id,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") let exists_implicit_name id = @@ -2161,7 +2165,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let loc = tm'.CAst.loc in match DAst.get tm', na with | GVar id, None when not (Id.Map.mem id (snd lvar)) -> Some id, CAst.make ?loc @@ Name id - | GRef (VarRef id, _), None -> Some id, CAst.make ?loc @@ Name id + | GRef (GlobRef.VarRef id, _), None -> Some id, CAst.make ?loc @@ Name id | _, None -> None, CAst.make Anonymous | _, Some ({ CAst.loc; v = na } as lna) -> None, lna in (* the "in" part *) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index dc6a1ae180..9bef31c7d8 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -115,12 +115,13 @@ let type_of_global_ref gr = if Typeclasses.is_class gr then "class" else + let open Names.GlobRef in match gr with - | Globnames.ConstRef cst -> - type_of_logical_kind (constant_kind cst) - | Globnames.VarRef v -> - "var" ^ type_of_logical_kind (Decls.variable_kind v) - | Globnames.IndRef ind -> + | ConstRef cst -> + type_of_logical_kind (constant_kind cst) + | VarRef v -> + "var" ^ type_of_logical_kind (Decls.variable_kind v) + | IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in if mib.Declarations.mind_record <> Declarations.NotRecord then begin match mib.Declarations.mind_finite with @@ -134,7 +135,7 @@ let type_of_global_ref gr = | BiFinite -> "variant" | CoFinite -> "coind" end - | Globnames.ConstructRef _ -> "constr" + | ConstructRef _ -> "constr" let remove_sections dir = let cwd = Lib.cwd_except_section () in diff --git a/interp/impargs.ml b/interp/impargs.ml index 9977b29310..0466efa991 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -394,18 +394,18 @@ let compute_mib_implicits flags kn = (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> (* No need to care about constraints here *) - let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in + let ty, _ = Typeops.type_of_global_in_context env (GlobRef.IndRef (kn,i)) in let r = Inductive.relevance_of_inductive env (kn,i) in Context.Rel.Declaration.LocalAssum (Context.make_annot (Name mip.mind_typename) r, ty)) mib.mind_packets) in let env_ar = Environ.push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in - ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), + let ar, _ = Typeops.type_of_global_in_context env (GlobRef.IndRef ind) in + ((GlobRef.IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), Array.mapi (fun j (ctx, cty) -> let c = of_constr (Term.it_mkProd_or_LetIn cty ctx) in - (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) + (GlobRef.ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets @@ -424,7 +424,7 @@ let compute_var_implicits flags id = (* Implicits of a global reference. *) -let compute_global_implicits flags = function +let compute_global_implicits flags = let open GlobRef in function | VarRef id -> compute_var_implicits flags id | ConstRef kn -> compute_constant_implicits flags kn | IndRef (kn,i) -> @@ -579,11 +579,11 @@ let declare_implicits local ref = let declare_var_implicits id = let flags = !implicit_args in - declare_implicits_gen ImplLocal flags (VarRef id) + declare_implicits_gen ImplLocal flags (GlobRef.VarRef id) let declare_constant_implicits con = let flags = !implicit_args in - declare_implicits_gen (ImplConstant flags) flags (ConstRef con) + declare_implicits_gen (ImplConstant flags) flags (GlobRef.ConstRef con) let declare_mib_implicits kn = let flags = !implicit_args in diff --git a/interp/notation.ml b/interp/notation.ml index d58125e29b..4a6ed75f10 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -305,7 +305,7 @@ let glob_constr_keys c = match DAst.get c with | _ -> [Oth] let cases_pattern_key c = match DAst.get c with - | PatCstr (ref,_,_) -> RefKey (canonical_gr (ConstructRef ref)) + | PatCstr (ref,_,_) -> RefKey (canonical_gr (GlobRef.ConstructRef ref)) | _ -> Oth let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) @@ -492,10 +492,10 @@ exception NotAValidPrimToken considered for parsing. *) let rec constr_of_glob env sigma g = match DAst.get g with - | Glob_term.GRef (ConstructRef c, _) -> + | Glob_term.GRef (GlobRef.ConstructRef c, _) -> let sigma,c = Evd.fresh_constructor_instance env sigma c in sigma,mkConstructU c - | Glob_term.GRef (IndRef c, _) -> + | Glob_term.GRef (GlobRef.IndRef c, _) -> let sigma,c = Evd.fresh_inductive_instance env sigma c in sigma,mkIndU c | Glob_term.GApp (gc, gcl) -> @@ -511,10 +511,10 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with let c = glob_of_constr token_kind ?loc env sigma c in let cel = List.map (glob_of_constr token_kind ?loc env sigma) (Array.to_list ca) in DAst.make ?loc (Glob_term.GApp (c, cel)) - | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None)) - | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) - | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) - | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) + | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.ConstructRef c, None)) + | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.ConstRef c, None)) + | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.IndRef ind, None)) + | Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None)) | Int i -> DAst.make ?loc (Glob_term.GInt i) | _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c)) @@ -836,7 +836,7 @@ let q_byte () = qualid_of_ref "core.byte.type" let unsafe_locate_ind q = match Nametab.locate q with - | IndRef i -> i + | GlobRef.IndRef i -> i | _ -> raise Not_found let locate_list () = unsafe_locate_ind (q_list ()) @@ -1219,7 +1219,7 @@ let uninterp_cases_pattern_notations c = keymap_find (cases_pattern_key c) !notations_key_table let uninterp_ind_pattern_notations ind = - keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table + keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table let availability_of_notation (ntn_scope,ntn) scopes = let f scope = diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index fdf12faa04..2fa78bb9f3 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -781,7 +781,7 @@ let rec pat_binder_of_term t = DAst.map (function | GVar id -> PatVar (Name id) | GApp (t, l) -> begin match DAst.get t with - | GRef (ConstructRef cstr,_) -> + | GRef (GlobRef.ConstructRef cstr,_) -> let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in let _,l = List.chop nparams l in PatCstr (cstr, List.map pat_binder_of_term l, Anonymous) @@ -1337,10 +1337,10 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = match DAst.get a1, a2 with | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) - | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 -> + | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 -> let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in sigma,(0,l) - | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2) + | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2) when eq_constructor r1 r2 -> let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in @@ -1362,9 +1362,9 @@ and match_cases_pattern_no_more_args metas sigma a1 a2 = let match_ind_pattern metas sigma ind pats a2 = match a2 with - | NRef (IndRef r2) when eq_ind ind r2 -> + | NRef (GlobRef.IndRef r2) when eq_ind ind r2 -> sigma,(0,pats) - | NApp (NRef (IndRef r2),l2) + | NApp (NRef (GlobRef.IndRef r2),l2) when eq_ind ind r2 -> let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 74fe5d1c80..5d36ceca38 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -52,7 +52,7 @@ let locate_global_with_alias ?(head=false) qid = let global_inductive_with_alias qid = try match locate_global_with_alias qid with - | IndRef ind -> ind + | Names.GlobRef.IndRef ind -> ind | ref -> user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" (pr_qualid qid ++ spc () ++ str "is not an inductive type.") diff --git a/library/coqlib.ml b/library/coqlib.ml index 7cd2e50274..b1e4ef2b00 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -13,7 +13,6 @@ open Util open Pp open Names open Libnames -open Globnames let make_dir l = DirPath.make (List.rev_map Id.of_string l) @@ -46,7 +45,7 @@ let has_ref s = CString.Map.mem s !table let check_ind_ref s ind = match CString.Map.find s !table with - | IndRef r -> eq_ind r ind + | GlobRef.IndRef r -> eq_ind r ind | _ -> false | exception Not_found -> false @@ -157,32 +156,32 @@ let type_of_id = Constant.make2 datatypes_module @@ Label.make "IDProp" let nat_kn = MutInd.make2 datatypes_module @@ Label.make "nat" let nat_path = Libnames.make_path (make_dir datatypes_module_name) (Id.of_string "nat") -let glob_nat = IndRef (nat_kn,0) +let glob_nat = GlobRef.IndRef (nat_kn,0) let path_of_O = ((nat_kn,0),1) let path_of_S = ((nat_kn,0),2) -let glob_O = ConstructRef path_of_O -let glob_S = ConstructRef path_of_S +let glob_O = GlobRef.ConstructRef path_of_O +let glob_S = GlobRef.ConstructRef path_of_S (** Booleans *) let bool_kn = MutInd.make2 datatypes_module @@ Label.make "bool" -let glob_bool = IndRef (bool_kn,0) +let glob_bool = GlobRef.IndRef (bool_kn,0) let path_of_true = ((bool_kn,0),1) let path_of_false = ((bool_kn,0),2) -let glob_true = ConstructRef path_of_true -let glob_false = ConstructRef path_of_false +let glob_true = GlobRef.ConstructRef path_of_true +let glob_false = GlobRef.ConstructRef path_of_false (** Equality *) let eq_kn = MutInd.make2 logic_module @@ Label.make "eq" -let glob_eq = IndRef (eq_kn,0) +let glob_eq = GlobRef.IndRef (eq_kn,0) let identity_kn = MutInd.make2 datatypes_module @@ Label.make "identity" -let glob_identity = IndRef (identity_kn,0) +let glob_identity = GlobRef.IndRef (identity_kn,0) let jmeq_kn = MutInd.make2 jmeq_module @@ Label.make "JMeq" -let glob_jmeq = IndRef (jmeq_kn,0) +let glob_jmeq = GlobRef.IndRef (jmeq_kn,0) (* Sigma data *) type coq_sigma_data = { diff --git a/library/globnames.ml b/library/globnames.ml index 71447c4b81..acb05f9ac0 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -12,12 +12,14 @@ open Names open Constr open Mod_subst -(*s Global reference is a kernel side type for all references together *) type global_reference = GlobRef.t = - | VarRef of variable (** A reference to the section-context. *) - | ConstRef of Constant.t (** A reference to the environment. *) - | IndRef of inductive (** A reference to an inductive type. *) - | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + | VarRef of variable [@ocaml.deprecated "Use Names.GlobRef.VarRef"] + | ConstRef of Constant.t [@ocaml.deprecated "Use Names.GlobRef.ConstRef"] + | IndRef of inductive [@ocaml.deprecated "Use Names.GlobRef.IndRef"] + | ConstructRef of constructor [@ocaml.deprecated "Use Names.GlobRef.ConstructRef"] +[@@ocaml.deprecated "Use Names.GlobRef.t"] + +open GlobRef let isVarRef = function VarRef _ -> true | _ -> false let isConstRef = function ConstRef _ -> true | _ -> false @@ -90,7 +92,7 @@ let printable_constr_of_global = function type syndef_name = KerName.t type extended_global_reference = - | TrueGlobal of global_reference + | TrueGlobal of GlobRef.t | SynDef of syndef_name (* We order [extended_global_reference] via their user part @@ -122,6 +124,6 @@ module ExtRefOrdered = struct end -type global_reference_or_constr = - | IsGlobal of global_reference +type global_reference_or_constr = + | IsGlobal of GlobRef.t | IsConstr of constr diff --git a/library/globnames.mli b/library/globnames.mli index 547755b088..fc0de96e36 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -12,12 +12,11 @@ open Names open Constr open Mod_subst -(** {6 Global reference is a kernel side type for all references together } *) type global_reference = GlobRef.t = - | VarRef of variable (** A reference to the section-context. *) - | ConstRef of Constant.t (** A reference to the environment. *) - | IndRef of inductive (** A reference to an inductive type. *) - | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + | VarRef of variable [@ocaml.deprecated "Use Names.GlobRef.VarRef"] + | ConstRef of Constant.t [@ocaml.deprecated "Use Names.GlobRef.ConstRef"] + | IndRef of inductive [@ocaml.deprecated "Use Names.GlobRef.IndRef"] + | ConstructRef of constructor [@ocaml.deprecated "Use Names.GlobRef.ConstructRef"] [@@ocaml.deprecated "Use Names.GlobRef.t"] val isVarRef : GlobRef.t -> bool diff --git a/library/keys.ml b/library/keys.ml index 30ecc9dfdb..9964992433 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -94,7 +94,7 @@ let subst_keys (subst,(k,k')) = (subst_key subst k, subst_key subst k') let discharge_key = function - | KGlob (VarRef _ as g) when Lib.is_in_section g -> None + | KGlob (GlobRef.VarRef _ as g) when Lib.is_in_section g -> None | x -> Some x let discharge_keys (_,(k,k')) = @@ -114,16 +114,15 @@ let declare_equiv_keys ref ref' = Lib.add_anonymous_leaf (inKeys (ref,ref')) let constr_key kind c = - let open Globnames in - try - let rec aux k = + try + let rec aux k = match kind k with - | Const (c, _) -> KGlob (ConstRef c) - | Ind (i, u) -> KGlob (IndRef i) - | Construct (c,u) -> KGlob (ConstructRef c) - | Var id -> KGlob (VarRef id) + | Const (c, _) -> KGlob (GlobRef.ConstRef c) + | Ind (i, u) -> KGlob (GlobRef.IndRef i) + | Construct (c,u) -> KGlob (GlobRef.ConstructRef c) + | Var id -> KGlob (GlobRef.VarRef id) | App (f, _) -> aux f - | Proj (p, _) -> KGlob (ConstRef (Projection.constant p)) + | Proj (p, _) -> KGlob (GlobRef.ConstRef (Projection.constant p)) | Cast (p, _, _) -> aux p | Lambda _ -> KLam | Prod _ -> KProd diff --git a/library/lib.ml b/library/lib.ml index 576e23c4f5..d461644d56 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -13,7 +13,6 @@ open CErrors open Util open Names open Libnames -open Globnames open Libobject open Context.Named.Declaration @@ -549,7 +548,7 @@ let empty_segment = { abstr_uctx = Univ.AUContext.empty; } -let section_segment_of_reference = function +let section_segment_of_reference = let open GlobRef in function | ConstRef c -> section_segment_of_constant c | IndRef (kn,_) | ConstructRef ((kn,_),_) -> section_segment_of_mutual_inductive kn @@ -558,7 +557,7 @@ let section_segment_of_reference = function let variable_section_segment_of_reference gr = (section_segment_of_reference gr).abstr_ctx -let section_instance = function +let section_instance = let open GlobRef in function | VarRef id -> let eq = function | Variable {id=id'} -> Names.Id.equal id id' @@ -647,7 +646,7 @@ let init () = (* Misc *) -let mp_of_global = function +let mp_of_global = let open GlobRef in function | VarRef id -> !lib_state.path_prefix.Nametab.obj_mp | ConstRef cst -> Names.Constant.modpath cst | IndRef ind -> Names.ind_modpath ind @@ -666,12 +665,12 @@ let rec split_modpath = function (dp, Names.Label.to_id l :: ids) let library_part = function - |VarRef id -> library_dp () - |ref -> dp_of_mp (mp_of_global ref) + | GlobRef.VarRef id -> library_dp () + | ref -> dp_of_mp (mp_of_global ref) let discharge_proj_repr = Projection.Repr.map_npars (fun mind npars -> - if not (is_in_section (IndRef (mind,0))) then mind, npars + if not (is_in_section (GlobRef.IndRef (mind,0))) then mind, npars else let modlist = replacement_context () in let _, newpars = Mindmap.find mind (snd modlist) in mind, npars + Array.length newpars) diff --git a/library/nametab.ml b/library/nametab.ml index 71ee7a6d5a..aed7d08ac1 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -392,6 +392,7 @@ let push_xref visibility sp xref = | _ -> begin if ExtRefTab.exists sp !the_ccitab then + let open GlobRef in match ExtRefTab.find sp !the_ccitab with | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) | TrueGlobal( ConstructRef _) as xref -> @@ -483,6 +484,7 @@ let completion_canditates qualid = (* Derived functions *) let locate_constant qid = + let open GlobRef in match locate_extended qid with | TrueGlobal (ConstRef kn) -> kn | _ -> raise Not_found @@ -517,6 +519,7 @@ let exists_universe kn = UnivTab.exists kn !the_univtab (* Reverse locate functions ***********************************************) let path_of_global ref = + let open GlobRef in match ref with | VarRef id -> make_path DirPath.empty id | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab @@ -542,6 +545,7 @@ let path_of_universe mp = (* Shortest qualid functions **********************************************) let shortest_qualid_of_global ?loc ctx ref = + let open GlobRef in match ref with | VarRef id -> make_qualid ?loc DirPath.empty id | _ -> @@ -570,6 +574,7 @@ let pr_global_env env ref = if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e let global_inductive qid = + let open GlobRef in match global qid with | IndRef ind -> ind | ref -> diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 9abf212443..6c845a75b2 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -15,7 +15,6 @@ open ModPath open Namegen open Nameops open Libnames -open Globnames open Table open Miniml open Mlutil @@ -629,21 +628,21 @@ let check_extract_ascii () = | Haskell -> "Prelude.Char" | _ -> raise Not_found in - String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type) + String.equal (find_custom (GlobRef.IndRef (ind_ascii, 0))) (char_type) with Not_found -> false let is_list_cons l = - List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l + List.for_all (function MLcons (_,GlobRef.ConstructRef(_,_),[]) -> true | _ -> false) l let is_native_char = function - | MLcons(_,ConstructRef ((kn,0),1),l) -> + | MLcons(_,GlobRef.ConstructRef ((kn,0),1),l) -> MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l | _ -> false let get_native_char c = let rec cumul = function | [] -> 0 - | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l) + | MLcons(_,GlobRef.ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l) | _ -> assert false in let l = match c with MLcons(_,_,l) -> l | _ -> assert false in diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index ca1520594d..551dbdc6fb 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -14,7 +14,6 @@ open Declarations open Names open ModPath open Libnames -open Globnames open Pp open CErrors open Util @@ -118,7 +117,7 @@ module Visit : VISIT = struct v.mp <- MPset.union (prefixes_mp mp) v.mp; v.mp_all <- MPset.add mp v.mp_all let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (KerName.modpath kn) - let add_ref = function + let add_ref = let open GlobRef in function | ConstRef c -> add_kn (Constant.user c) | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (MutInd.user ind) | VarRef _ -> assert false @@ -761,7 +760,7 @@ let show_extraction ~pstate = let ast, ty = extract_constr env sigma t in let mp = Lib.current_mp () in let l = Label.of_id (Proof_global.get_proof_name pstate) in - let fake_ref = ConstRef (Constant.make2 mp l) in + let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in let decl = Dterm (fake_ref, ast, ty) in print_one_decl [] mp decl in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index d0ad21a13e..78c6255c1e 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -24,7 +24,6 @@ open Termops open Inductiveops open Recordops open Namegen -open Globnames open Miniml open Table open Mlutil @@ -303,7 +302,7 @@ let rec extract_type env sg db j c args = else let n' = List.nth db (n-1) in if Int.equal n' 0 then Tunknown else Tvar n') | Const (kn,u) -> - let r = ConstRef kn in + let r = GlobRef.ConstRef kn in let typ = type_of env sg (EConstr.mkConstU (kn,u)) in (match flag_of_type env sg typ with | (Logic,_) -> assert false (* Cf. logical cases above *) @@ -311,7 +310,7 @@ let rec extract_type env sg db j c args = let mlt = extract_type_app env sg db (r, type_sign env sg typ) args in (match (lookup_constant kn env).const_body with | Undef _ | OpaqueDef _ | Primitive _ -> mlt - | Def _ when is_custom (ConstRef kn) -> mlt + | Def _ when is_custom (GlobRef.ConstRef kn) -> mlt | Def lbody -> let newc = applistc (get_body lbody) args in let mlt' = extract_type env sg db j newc [] in @@ -331,7 +330,7 @@ let rec extract_type env sg db j c args = extract_type env sg db j newc [])) | Ind ((kn,i),u) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in - extract_type_app env sg db (IndRef (kn,i),s) args + extract_type_app env sg db (GlobRef.IndRef (kn,i),s) args | Proj (p,t) -> (* Let's try to reduce, if it hasn't already been done. *) if Projection.unfolded p then Tunknown @@ -346,7 +345,7 @@ let rec extract_type env sg db j c args = | LocalDef (_,body,_) -> extract_type env sg db j (EConstr.applist (body,args)) [] | LocalAssum (_,ty) -> - let r = VarRef v in + let r = GlobRef.VarRef v in (match flag_of_type env sg ty with | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> @@ -405,7 +404,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) extract_really_ind env kn mib with SingletonInductiveBecomesProp id -> (* TODO : which inductive is concerned in the block ? *) - error_singleton_become_prop id (Some (IndRef (kn,0))) + error_singleton_become_prop id (Some (GlobRef.IndRef (kn,0))) (* Then the real function *) @@ -481,7 +480,7 @@ and extract_really_ind env kn mib = let ind_info = try let ip = (kn, 0) in - let r = IndRef ip in + let r = GlobRef.IndRef ip in if is_custom r then raise (I Standard); if mib.mind_finite == CoFinite then raise (I Coinductive); if not (Int.equal mib.mind_ntypes 1) then raise (I Standard); @@ -519,7 +518,7 @@ and extract_really_ind env kn mib = (* Is it safe to use [id] for projections [foo.id] ? *) if List.for_all ((==) Keep) (type2signature env typ) then projs := Cset.add knp !projs; - Some (ConstRef knp) :: (select_fields l typs) + Some (GlobRef.ConstRef knp) :: (select_fields l typs) | _ -> assert false in let field_glob = select_fields field_names typ @@ -565,7 +564,7 @@ and extract_type_cons env sg db dbmap c i = (*s Recording the ML type abbreviation of a Coq type scheme constant. *) -and mlt_env env r = match r with +and mlt_env env r = let open GlobRef in match r with | IndRef _ | ConstructRef _ | VarRef _ -> None | ConstRef kn -> let cb = Environ.lookup_constant kn env in @@ -688,7 +687,7 @@ let rec extract_term env sg mle mlt c args = | LocalDef (_,_,ty) -> ty in let vty = extract_type env sg [] 0 ty [] in - let extract_var mlt = put_magic (mlt,vty) (MLglob (VarRef v)) in + let extract_var mlt = put_magic (mlt,vty) (MLglob (GlobRef.VarRef v)) in extract_app env sg mle mlt extract_var args | Int i -> assert (args = []); MLuint i | Ind _ | Prod _ | Sort _ -> assert false @@ -746,10 +745,10 @@ and extract_cst_app env sg mle mlt kn args = (* Second, is the resulting type compatible with the expected type [mlt] ? *) let magic2 = needs_magic (a, mlt) in (* The internal head receives a magic if [magic1] *) - let head = put_magic_if magic1 (MLglob (ConstRef kn)) in + let head = put_magic_if magic1 (MLglob (GlobRef.ConstRef kn)) in (* Now, the extraction of the arguments. *) let s_full = type2signature env (snd schema) in - let s_full = sign_with_implicits (ConstRef kn) s_full 0 in + let s_full = sign_with_implicits (GlobRef.ConstRef kn) s_full 0 in let s = sign_no_final_keeps s_full in let ls = List.length s in let la = List.length args in @@ -762,7 +761,7 @@ and extract_cst_app env sg mle mlt kn args = (* for better optimisations later, we discard dependent args of projections and replace them by fake args that will be removed during final pretty-print. *) - let l,l' = List.chop (projection_arity (ConstRef kn)) mla in + let l,l' = List.chop (projection_arity (GlobRef.ConstRef kn)) mla in if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l' else mla with e when CErrors.noncritical e -> mla @@ -807,11 +806,11 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args = let nb_tvars = List.length oi.ip_vars and types = List.map (expand env) oi.ip_types.(j-1) in let list_tvar = List.map (fun i -> Tvar i) (List.interval 1 nb_tvars) in - let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in + let type_cons = type_recomp (types, Tglob (GlobRef.IndRef ip, list_tvar)) in let type_cons = instantiation (nb_tvars, type_cons) in (* Then, the usual variables [s], [ls], [la], ... *) let s = List.map (type2sign env) types in - let s = sign_with_implicits (ConstructRef cp) s params_nb in + let s = sign_with_implicits (GlobRef.ConstructRef cp) s params_nb in let ls = List.length s in let la = List.length args in assert (la <= ls + params_nb); @@ -831,8 +830,8 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args = | Tglob (_,l) -> List.map type_simpl l | _ -> assert false in - let typ = Tglob(IndRef ip, typeargs) in - put_magic_if magic1 (MLcons (typ, ConstructRef cp, mla)) + let typ = Tglob(GlobRef.IndRef ip, typeargs) in + put_magic_if magic1 (MLcons (typ, GlobRef.ConstructRef cp, mla)) in (* Different situations depending of the number of arguments: *) if la < params_nb then @@ -880,11 +879,11 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt = let oi = mi.ind_packets.(i) in let metas = Array.init (List.length oi.ip_vars) new_meta in (* The extraction of the head. *) - let type_head = Tglob (IndRef ip, Array.to_list metas) in + let type_head = Tglob (GlobRef.IndRef ip, Array.to_list metas) in let a = extract_term env sg mle type_head c [] in (* The extraction of each branch. *) let extract_branch i = - let r = ConstructRef (ip,i+1) in + let r = GlobRef.ConstructRef (ip,i+1) in (* The types of the arguments of the corresponding constructor. *) let f t = type_subst_vect metas (expand env t) in let l = List.map f oi.ip_types.(i) in @@ -909,7 +908,7 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt = else (* Standard case: we apply [extract_branch]. *) let typs = List.map type_simpl (Array.to_list metas) in - let typ = Tglob (IndRef ip,typs) in + let typ = Tglob (GlobRef.IndRef ip,typs) in MLcase (typ, a, Array.init br_size extract_branch) (*s Extraction of a (co)-fixpoint. *) @@ -960,7 +959,7 @@ let extract_std_constant env sg kn body typ = let l,t' = type_decomp (expand env (var2var' t)) in let s = List.map (type2sign env) l in (* Check for user-declared implicit information *) - let s = sign_with_implicits (ConstRef kn) s 0 in + let s = sign_with_implicits (GlobRef.ConstRef kn) s 0 in (* Decomposing the top level lambdas of [body]. If there isn't enough, it's ok, as long as remaining args aren't to be pruned (and initial lambdas aren't to be all @@ -1015,7 +1014,7 @@ let extract_axiom env sg kn typ = let l,_ = type_decomp (expand env (var2var' t)) in let s = List.map (type2sign env) l in (* Check for user-declared implicit information *) - let s = sign_with_implicits (ConstRef kn) s 0 in + let s = sign_with_implicits (GlobRef.ConstRef kn) s 0 in type_expunge_from_sign env s t let extract_fixpoint env sg vkn (fi,ti,ci) = @@ -1034,10 +1033,10 @@ let extract_fixpoint env sg vkn (fi,ti,ci) = terms.(i) <- e; types.(i) <- t; with SingletonInductiveBecomesProp id -> - error_singleton_become_prop id (Some (ConstRef vkn.(i))) + error_singleton_become_prop id (Some (GlobRef.ConstRef vkn.(i))) done; current_fixpoints := []; - Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) + Dfix (Array.map (fun kn -> GlobRef.ConstRef kn) vkn, terms, types) (** Because of automatic unboxing the easy way [mk_def c] on the constant body of primitive projections doesn't work. We pretend @@ -1095,7 +1094,7 @@ let fake_match_projection env p = let extract_constant env kn cb = let sg = Evd.from_env env in - let r = ConstRef kn in + let r = GlobRef.ConstRef kn in let typ = EConstr.of_constr cb.const_type in let warn_info () = if not (is_custom r) then add_info_axiom r in let warn_log () = if not (constant_has_body cb) then add_log_axiom r @@ -1150,11 +1149,11 @@ let extract_constant env kn cb = if access_opaque () then mk_def (get_opaque env c) else mk_ax ()) with SingletonInductiveBecomesProp id -> - error_singleton_become_prop id (Some (ConstRef kn)) + error_singleton_become_prop id (Some (GlobRef.ConstRef kn)) let extract_constant_spec env kn cb = let sg = Evd.from_env env in - let r = ConstRef kn in + let r = GlobRef.ConstRef kn in let typ = EConstr.of_constr cb.const_type in try match flag_of_type env sg typ with @@ -1173,7 +1172,7 @@ let extract_constant_spec env kn cb = let t = snd (record_constant_type env sg kn (Some typ)) in Sval (r, type_expunge env t) with SingletonInductiveBecomesProp id -> - error_singleton_become_prop id (Some (ConstRef kn)) + error_singleton_become_prop id (Some (GlobRef.ConstRef kn)) let extract_with_type env sg c = try @@ -1205,7 +1204,7 @@ let extract_inductive env kn = let ind = extract_ind env kn in add_recursors env kn; let f i j l = - let implicits = implicits_of_global (ConstructRef ((kn,i),j+1)) in + let implicits = implicits_of_global (GlobRef.ConstructRef ((kn,i),j+1)) in let rec filter i = function | [] -> [] | t::l -> diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index a62fb1a728..e4efbcff0c 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -14,7 +14,6 @@ open Pp open CErrors open Util open Names -open Globnames open Table open Miniml open Mlutil @@ -110,7 +109,7 @@ let rec pp_type par vl t = (try Id.print (List.nth vl (pred i)) with Failure _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r - | Tglob (IndRef(kn,0),l) + | Tglob (GlobRef.IndRef(kn,0),l) when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> pp_type true vl (List.hd l) | Tglob (r,l) -> @@ -271,7 +270,7 @@ let pp_logical_ind packet = prvect_with_sep spc Id.print packet.ip_consnames) let pp_singleton kn packet = - let name = pp_global Type (IndRef (kn,0)) in + let name = pp_global Type (GlobRef.IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ name ++ spc () ++ prlist_with_sep spc Id.print l ++ @@ -291,14 +290,14 @@ let pp_one_ind ip pl cv = (fun () -> (str " ")) (pp_type true pl) l)) in str (if Array.is_empty cv then "type " else "data ") ++ - pp_global Type (IndRef ip) ++ + pp_global Type (GlobRef.IndRef ip) ++ prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++ if Array.is_empty cv then str " () -- empty inductive" else (fnl () ++ str " " ++ v 0 (str " " ++ prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor - (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv))) + (Array.mapi (fun i c -> GlobRef.ConstructRef (ip,i+1),c) cv))) let rec pp_ind first kn i ind = if i >= Array.length ind.ind_packets then @@ -306,7 +305,7 @@ let rec pp_ind first kn i ind = else let ip = (kn,i) in let p = ind.ind_packets.(i) in - if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind + if is_custom (GlobRef.IndRef (kn,i)) then pp_ind first kn (i+1) ind else if p.ip_logical then pp_logical_ind p ++ pp_ind first kn (i+1) ind diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index f88d29e9ed..fba6b7c780 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -1,7 +1,6 @@ open Pp open Util open Names -open Globnames open Table open Miniml open Mlutil @@ -200,10 +199,10 @@ and json_function env t = let json_ind ip pl cv = json_dict [ ("what", json_str "decl:ind"); - ("name", json_global Type (IndRef ip)); + ("name", json_global Type (GlobRef.IndRef ip)); ("argnames", json_list (List.map json_id pl)); ("constructors", json_listarr (Array.mapi (fun idx c -> json_dict [ - ("name", json_global Cons (ConstructRef (ip, idx+1))); + ("name", json_global Cons (GlobRef.ConstructRef (ip, idx+1))); ("argtypes", json_list (List.map (json_type pl) c)) ]) cv)) ] diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index a8d766cd6e..2d5872718f 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -12,7 +12,6 @@ open Util open Names open Libnames -open Globnames open Table open Miniml (*i*) @@ -668,11 +667,11 @@ let is_regular_match br = | _ -> raise Impossible in let ind = match get_r br.(0) with - | ConstructRef (ind,_) -> ind + | GlobRef.ConstructRef (ind,_) -> ind | _ -> raise Impossible in let is_ref i tr = match get_r tr with - | ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) + | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) | _ -> false in Array.for_all_i is_ref 0 br @@ -819,11 +818,11 @@ let rec tmp_head_lams = function *) let rec ast_glob_subst s t = match t with - | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> + | MLapp ((MLglob ((GlobRef.ConstRef kn) as refe)) as f, a) -> let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in (try linear_beta_red a (Refmap'.find refe s) with Not_found -> MLapp (f, a)) - | MLglob ((ConstRef kn) as refe) -> + | MLglob ((GlobRef.ConstRef kn) as refe) -> (try Refmap'.find refe s with Not_found -> t) | _ -> ast_map (ast_glob_subst s) t @@ -1504,7 +1503,7 @@ open Declareops let inline_test r t = if not (auto_inline ()) then false else - let c = match r with ConstRef c -> c | _ -> assert false in + let c = match r with GlobRef.ConstRef c -> c | _ -> assert false in let has_body = try constant_has_body (Global.lookup_constant c) with Not_found -> false @@ -1534,7 +1533,7 @@ let manual_inline_set = Cset_env.empty let manual_inline = function - | ConstRef c -> Cset_env.mem c manual_inline_set + | GlobRef.ConstRef c -> Cset_env.mem c manual_inline_set | _ -> false (* If the user doesn't say he wants to keep [t], we inline in two cases: diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index bded698ea7..6b1eef7abb 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -10,7 +10,6 @@ open Names open ModPath -open Globnames open CErrors open Util open Miniml @@ -42,7 +41,7 @@ let se_iter do_decl do_spec do_mp = let mp_w = List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in + let r = GlobRef.ConstRef (Constant.make2 mp_w (Label.of_id l')) in mt_iter mt; do_spec (Stype(r,l,Some t)) | MTwith (mt,ML_With_module(idl,mp))-> let mp_mt = msid_of_mt mt in @@ -113,12 +112,12 @@ let ast_iter_references do_term do_cons do_type a = let ind_iter_references do_term do_cons do_type kn ind = let type_iter = type_iter_references do_type in - let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in + let cons_iter cp l = do_cons (GlobRef.ConstructRef cp); List.iter type_iter l in let packet_iter ip p = - do_type (IndRef ip); + do_type (GlobRef.IndRef ip); if lang () == Ocaml then (match ind.ind_equiv with - | Miniml.Equiv kne -> do_type (IndRef (MutInd.make1 kne, snd ip)); + | Miniml.Equiv kne -> do_type (GlobRef.IndRef (MutInd.make1 kne, snd ip)); | _ -> ()); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in @@ -258,7 +257,7 @@ let dfix_to_mlfix rv av i = let s = make_subst (Array.length rv - 1) Refmap'.empty in let rec subst n t = match t with - | MLglob ((ConstRef kn) as refe) -> + | MLglob ((GlobRef.ConstRef kn) as refe) -> (try MLrel (n + (Refmap'.find refe s)) with Not_found -> t) | _ -> ast_map_lift subst n t in @@ -309,7 +308,7 @@ and optim_me to_appear s = function For non-library extraction, we recompute a minimal set of dependencies for first-level definitions (no module pruning yet). *) -let base_r = function +let base_r = let open GlobRef in function | ConstRef c as r -> r | IndRef (kn,_) -> IndRef (kn,0) | ConstructRef ((kn,_),_) -> IndRef (kn,0) @@ -327,7 +326,7 @@ let reset_needed, add_needed, add_needed_mp, found_needed, is_needed = Refset'.mem r !needed || MPset.mem (modpath_of_r r) !needed_mps)) let declared_refs = function - | Dind (kn,_) -> [IndRef (kn,0)] + | Dind (kn,_) -> [GlobRef.IndRef (kn,0)] | Dtype (r,_,_) -> [r] | Dterm (r,_,_) -> [r] | Dfix (rv,_,_) -> Array.to_list rv diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 21a8b8e5fb..75fb35192b 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -15,7 +15,6 @@ open CErrors open Util open Names open ModPath -open Globnames open Table open Miniml open Mlutil @@ -142,7 +141,7 @@ let get_infix r = let s = find_custom r in String.sub s 1 (String.length s - 2) -let get_ind = function +let get_ind = let open GlobRef in function | IndRef _ as r -> r | ConstructRef (ind,_) -> IndRef ind | _ -> assert false @@ -166,7 +165,7 @@ let pp_type par vl t = | Tglob (r,[a1;a2]) when is_infix r -> pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2) | Tglob (r,[]) -> pp_global Type r - | Tglob (IndRef(kn,0),l) + | Tglob (GlobRef.IndRef(kn,0),l) when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> pp_tuple_light pp_rec l | Tglob (r,l) -> @@ -467,7 +466,7 @@ let pp_Dfix (rv,c,t) = let pp_equiv param_list name = function | NoEquiv, _ -> mt () | Equiv kn, i -> - str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (MutInd.make1 kn,i)) + str " = " ++ pp_parameters param_list ++ pp_global Type (GlobRef.IndRef (MutInd.make1 kn,i)) | RenEquiv ren, _ -> str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name @@ -494,7 +493,7 @@ let pp_logical_ind packet = fnl () let pp_singleton kn packet = - let name = pp_global Type (IndRef (kn,0)) in + let name = pp_global Type (GlobRef.IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ @@ -502,7 +501,7 @@ let pp_singleton kn packet = Id.print packet.ip_consnames.(0))) let pp_record kn fields ip_equiv packet = - let ind = IndRef (kn,0) in + let ind = GlobRef.IndRef (kn,0) in let name = pp_global Type ind in let fieldnames = pp_fields ind fields in let l = List.combine fieldnames packet.ip_types.(0) in @@ -525,13 +524,13 @@ let pp_ind co kn ind = let nextkwd = fnl () ++ str "and " in let names = Array.mapi (fun i p -> if p.ip_logical then mt () else - pp_global Type (IndRef (kn,i))) + pp_global Type (GlobRef.IndRef (kn,i))) ind.ind_packets in let cnames = Array.mapi (fun i p -> if p.ip_logical then [||] else - Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1))) + Array.mapi (fun j _ -> pp_global Cons (GlobRef.ConstructRef ((kn,i),j+1))) p.ip_types) ind.ind_packets in @@ -541,7 +540,7 @@ let pp_ind co kn ind = let ip = (kn,i) in let ip_equiv = ind.ind_equiv, i in let p = ind.ind_packets.(i) in - if is_custom (IndRef ip) then pp (i+1) kwd + if is_custom (GlobRef.IndRef ip) then pp (i+1) kwd else if p.ip_logical then pp_logical_ind p ++ pp (i+1) kwd else kwd ++ (if co then pp_coind p.ip_vars names.(i) else mt ()) ++ @@ -672,7 +671,7 @@ and pp_module_type params = function let mp_w = List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (Constant.make2 mp_w (Label.of_id l)) in + let r = GlobRef.ConstRef (Constant.make2 mp_w (Label.of_id l)) in push_visible mp_mt []; let pp_w = str " with type " ++ ids ++ pp_global Type r in pop_visible(); diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index b09a81e1c8..96a3d00dc2 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -30,12 +30,12 @@ module Refset' = GlobRef.Set_env (*S Utilities about [module_path] and [kernel_names] and [global_reference] *) -let occur_kn_in_ref kn = function +let occur_kn_in_ref kn = let open GlobRef in function | IndRef (kn',_) | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' | ConstRef _ | VarRef _ -> false -let repr_of_r = function +let repr_of_r = let open GlobRef in function | ConstRef kn -> Constant.repr2 kn | IndRef (kn,_) | ConstructRef ((kn,_),_) -> MutInd.repr2 kn @@ -151,7 +151,7 @@ let init_inductive_kinds () = inductive_kinds := Mindmap_env.empty let add_inductive_kind kn k = inductive_kinds := Mindmap_env.add kn k !inductive_kinds let is_coinductive r = - let kn = match r with + let kn = let open GlobRef in match r with | ConstructRef ((kn,_),_) -> kn | IndRef (kn,_) -> kn | _ -> assert false @@ -164,7 +164,7 @@ let is_coinductive_type = function | _ -> false let get_record_fields r = - let kn = match r with + let kn = let open GlobRef in match r with | ConstructRef ((kn,_),_) -> kn | IndRef (kn,_) -> kn | _ -> assert false @@ -201,7 +201,7 @@ let add_recursors env ind = mib.mind_packets let is_recursor = function - | ConstRef c -> KNset.mem (Constant.canonical c) !recursors + | GlobRef.ConstRef c -> KNset.mem (Constant.canonical c) !recursors | _ -> false (*s Record tables. *) @@ -210,7 +210,7 @@ let is_recursor = function let projs = ref (GlobRef.Map.empty : (inductive*int) GlobRef.Map.t) let init_projs () = projs := GlobRef.Map.empty -let add_projection n kn ip = projs := GlobRef.Map.add (ConstRef kn) (ip,n) !projs +let add_projection n kn ip = projs := GlobRef.Map.add (GlobRef.ConstRef kn) (ip,n) !projs let is_projection r = GlobRef.Map.mem r !projs let projection_arity r = snd (GlobRef.Map.find r !projs) let projection_info r = GlobRef.Map.find r !projs @@ -264,6 +264,7 @@ let safe_basename_of_global r = with Not_found -> anomaly (Pp.str "Inductive object unknown to extraction and not globally visible.") in + let open GlobRef in match r with | ConstRef kn -> Label.to_id (Constant.label kn) | IndRef (kn,0) -> Label.to_id (MutInd.label kn) @@ -286,7 +287,7 @@ let safe_pr_global r = str (string_of_global r) let safe_pr_long_global r = try Printer.pr_global r with Not_found -> match r with - | ConstRef kn -> + | GlobRef.ConstRef kn -> let mp,l = Constant.repr2 kn in str ((ModPath.to_string mp)^"."^(Label.to_string l)) | _ -> assert false @@ -658,7 +659,7 @@ let extraction_inline b l = let refs = List.map Smartlocate.global_with_alias l in List.iter (fun r -> match r with - | ConstRef _ -> () + | GlobRef.ConstRef _ -> () | _ -> error_constant r) refs; Lib.add_anonymous_leaf (inline_extraction (b,refs)) @@ -666,7 +667,7 @@ let extraction_inline b l = let print_extraction_inline () = let (i,n)= !inline_table in - let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in + let i'= Refset'.filter (function GlobRef.ConstRef _ -> true | _ -> false) i in (str "Extraction Inline:" ++ fnl () ++ Refset'.fold (fun r p -> @@ -823,8 +824,8 @@ let indref_of_match pv = if Array.is_empty pv then raise Not_found; let (_,pat,_) = pv.(0) in match pat with - | Pusual (ConstructRef (ip,_)) -> IndRef ip - | Pcons (ConstructRef (ip,_),_) -> IndRef ip + | Pusual (GlobRef.ConstructRef (ip,_)) -> GlobRef.IndRef ip + | Pcons (GlobRef.ConstructRef (ip,_),_) -> GlobRef.IndRef ip | _ -> raise Not_found let is_custom_match pv = @@ -852,9 +853,9 @@ let extract_constant_inline inline r ids s = check_inside_section (); let g = Smartlocate.global_with_alias r in match g with - | ConstRef kn -> + | GlobRef.ConstRef kn -> let env = Global.env () in - let typ, _ = Typeops.type_of_global_in_context env (ConstRef kn) in + let typ, _ = Typeops.type_of_global_in_context env (GlobRef.ConstRef kn) in let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin @@ -871,7 +872,7 @@ let extract_inductive r s l optstr = let g = Smartlocate.global_with_alias r in Dumpglob.add_glob ?loc:r.CAst.loc g; match g with - | IndRef ((kn,i) as ip) -> + | GlobRef.IndRef ((kn,i) as ip) -> let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets.(i).mind_consnames in if not (Int.equal n (List.length l)) then error_nb_cons (); @@ -881,7 +882,7 @@ let extract_inductive r s l optstr = optstr; List.iteri (fun j s -> - let g = ConstructRef (ip,succ j) in + let g = GlobRef.ConstructRef (ip,succ j) in Lib.add_anonymous_leaf (inline_extraction (true,[g])); Lib.add_anonymous_leaf (in_customs (g,[],s))) l | _ -> error_inductive g diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 2d5ea9536c..fb363b9393 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -15,7 +15,6 @@ open EConstr open Vars open Util open Declarations -open Globnames module RelDecl = Context.Rel.Declaration @@ -124,7 +123,7 @@ type side = Hyp | Concl | Hint let no_atoms = (false,{positive=[];negative=[]}) -let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *) +let dummy_id=GlobRef.VarRef (Id.of_string "_") (* "_" cannot be parsed *) let build_atoms env sigma metagen side cciterm = let trivial =ref false diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index bdf339a488..e134562702 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -15,12 +15,11 @@ open Rules open Instances open Tacmach.New open Tacticals.New -open Globnames let update_flags ()= let open TransparentState in let f accu coe = match coe.Classops.coe_value with - | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst } + | Names.GlobRef.ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst } | _ -> accu in let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index f3a16cd13e..79386f7ac9 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -20,7 +20,6 @@ open Proofview.Notations open Termops open Formula open Sequent -open Globnames module NamedDecl = Context.Named.Declaration @@ -48,7 +47,7 @@ let wrap n b continue seq = List.exists (occur_var_in_decl env sigma id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula env sigma Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in + add_formula env sigma Hyp (GlobRef.VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in let seq1=aux n nc [] in let seq2=if b then add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in @@ -56,7 +55,7 @@ let wrap n b continue seq = end let clear_global=function - VarRef id-> clear [id] + | GlobRef.VarRef id-> clear [id] | _->tclIDTAC (* connection rules *) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 0efb27e3f0..08298bf02c 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -14,7 +14,6 @@ open Tacticals open Tactics open Indfun_common open Libnames -open Globnames open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -1027,7 +1026,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a update_Function {finfos with equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with - ConstRef c -> c + GlobRef.ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) } diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index cb7a509829..d34faa22fa 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -84,7 +84,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in let rel_as_kn = fst (match princ_type_info.indref with - | Some (Globnames.IndRef ind) -> ind + | Some (GlobRef.IndRef ind) -> ind | _ -> user_err Pp.(str "Not a valid predicate") ) in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index bcad6cedf1..6dc01a9f8f 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -6,7 +6,6 @@ open Context open Vars open Glob_term open Glob_ops -open Globnames open Indfun_common open CErrors open Util @@ -312,7 +311,7 @@ let build_constructors_of_type ind' argl = let npar = mib.Declarations.mind_nparams in Array.mapi (fun i _ -> let construct = ind',i+1 in - let constructref = ConstructRef(construct) in + let constructref = GlobRef.ConstructRef(construct) in let _implicit_positions_of_cst = Impargs.implicits_of_global constructref in @@ -328,7 +327,7 @@ let build_constructors_of_type ind' argl = List.make npar (mkGHole ()) @ argl in let pat_as_term = - mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) + mkGApp(mkGRef (GlobRef.ConstructRef(ind',i+1)),argl) in cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term ) @@ -438,7 +437,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function let patl_as_term = List.map2 (pattern_to_term_and_type env) (List.rev cs_args_types) patternl in - mkGApp(mkGRef(ConstructRef constr), + mkGApp(mkGRef(GlobRef.ConstructRef constr), implicit_args@patl_as_term ) ) @@ -992,7 +991,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = in mkGProd(n,t,new_b),id_to_exclude with Continue -> - let jmeq = Globnames.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in + let jmeq = GlobRef.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in let ind,args' = Inductiveops.find_inductive env Evd.(from_env env) ty' in let mib,_ = Global.lookup_inductive (fst ind) in @@ -1001,7 +1000,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = ((Util.List.chop nparam args')) in let rt_typ = DAst.make @@ - GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None), + GApp(DAst.make @@ GRef (GlobRef.IndRef (fst ind),None), (List.map (fun p -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 7b758da8e8..d36d86a65b 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -375,7 +375,7 @@ let rec pattern_to_term pt = DAst.with_val (function let patl_as_term = List.map pattern_to_term patternl in - mkGApp(mkGRef(Globnames.ConstructRef constr), + mkGApp(mkGRef(GlobRef.ConstructRef constr), implicit_args@patl_as_term ) ) pt diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 48e3129599..99efe3e5e2 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -8,7 +8,6 @@ open EConstr open Pp open Indfun_common open Libnames -open Globnames open Glob_term open Declarations open Tactypes @@ -59,7 +58,7 @@ let functional_induction with_clean c princl pat = let princ,g' = (* then we get the principle *) try let g',princ = - Tacmach.pf_eapply (Evd.fresh_global) g (Globnames.ConstRef (Option.get princ_option )) in + Tacmach.pf_eapply (Evd.fresh_global) g (GlobRef.ConstRef (Option.get princ_option )) in princ,g' with Option.IsNone -> (*i If there is not default lemma defined then, @@ -836,7 +835,7 @@ let make_graph (f_ref : GlobRef.t) = let sigma = Evd.from_env env in let c,c_body = match f_ref with - | ConstRef c -> + | GlobRef.ConstRef c -> begin try c,Global.lookup_constant c with Not_found -> raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) ) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index c906670dc0..a119586f7b 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -2,7 +2,6 @@ open Names open Pp open Constr open Libnames -open Globnames open Refiner let mk_prefix pre id = Id.of_string (pre^(Id.to_string id)) @@ -31,12 +30,12 @@ let locate qid = Nametab.locate qid let locate_ind ref = match locate ref with - | IndRef x -> x + | GlobRef.IndRef x -> x | _ -> raise Not_found let locate_constant ref = match locate ref with - | ConstRef x -> x + | GlobRef.ConstRef x -> x | _ -> raise Not_found @@ -129,10 +128,10 @@ let save name const ?hook uctx scope kind = | Discharge -> let c = SectionLocalDef const in let () = declare_variable ~name ~kind c in - VarRef name + GlobRef.VarRef name | Global local -> let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in - ConstRef kn + GlobRef.ConstRef kn in DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r }); definition_message name @@ -275,7 +274,7 @@ let pr_info env sigma f_info = str "function_constant_type := " ++ (try Printer.pr_lconstr_env env sigma - (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant))) + (fst (Typeops.type_of_global_in_context env (GlobRef.ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst env sigma f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst env sigma f_info.completeness_lemma ++ fnl () ++ @@ -299,7 +298,7 @@ let in_Function : function_info -> Libobject.obj = let find_or_none id = try Some - (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.") + (match Nametab.locate (qualid_of_ident id) with GlobRef.ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.") ) with Not_found -> None @@ -328,7 +327,7 @@ let add_Function is_general f = and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) - with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.") + with | GlobRef.IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.") in let finfos = { function_constant = f; @@ -433,8 +432,8 @@ let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *) match r with - ConstRef sp -> EvalConstRef sp - | VarRef id -> EvalVarRef id + GlobRef.ConstRef sp -> EvalConstRef sp + | GlobRef.VarRef id -> EvalVarRef id | _ -> assert false;; let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8fa001278b..d4cc31c0af 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -19,7 +19,6 @@ open Context open EConstr open Vars open Pp -open Globnames open Tacticals open Tactics open Indfun_common @@ -93,7 +92,7 @@ let make_eq () = let generate_type evd g_to_f f graph i = (*i we deduce the number of arguments of the function and its returned type from the graph i*) let evd',graph = - Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph))) + Evd.fresh_global (Global.env ()) !evd (GlobRef.IndRef (fst (destInd !evd graph))) in evd:=evd'; let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in @@ -165,7 +164,7 @@ let find_induction_principle evd f = match infos.rect_lemma with | None -> raise Not_found | Some rect_lemma -> - let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in + let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (GlobRef.ConstRef rect_lemma) in let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in evd:=evd'; rect_lemma,typ @@ -978,7 +977,7 @@ let error msg = user_err Pp.(str msg) let invfun qhyp f = let f = match f with - | ConstRef f -> f + | GlobRef.ConstRef f -> f | _ -> raise (CErrors.UserError(None,str "Not a function")) in try diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f4edbda04a..2d8f075aba 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -67,7 +67,7 @@ let find_reference sl s = let declare_fun name kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in - ConstRef(declare_constant ~name ~kind (DefinitionEntry ce)) + GlobRef.ConstRef(declare_constant ~name ~kind (DefinitionEntry ce)) let defined lemma = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None @@ -95,7 +95,7 @@ let type_of_const sigma t = let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s) let const_of_ref = function - ConstRef kn -> kn + GlobRef.ConstRef kn -> kn | _ -> anomaly (Pp.str "ConstRef expected.") (* Generic values *) @@ -1312,7 +1312,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type 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 + GlobRef.ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.") in let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in @@ -1455,7 +1455,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let open CVars in let opacity = match terminate_ref with - | ConstRef c -> is_opaque_constant c + | GlobRef.ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in let evd = Evd.from_ctx uctx in diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index db8d09b79e..0e38ce575b 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -194,7 +194,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_evaluable_reference = function | EvalVarRef id -> pr_id id - | EvalConstRef sp -> pr_global (Globnames.ConstRef sp) + | EvalConstRef sp -> pr_global (GlobRef.ConstRef sp) let pr_quantified_hypothesis = function | AnonHyp n -> int n @@ -385,7 +385,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_evaluable_reference_env env = function | EvalVarRef id -> pr_id id | EvalConstRef sp -> - Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp) + Nametab.pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef sp) let pr_as_disjunctive_ipat prc ipatl = keyword "as" ++ spc () ++ diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 13844c2707..726752a2bf 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -24,7 +24,6 @@ open Tactics open Pretype_errors open Typeclasses open Constrexpr -open Globnames open Evd open Tactypes open Locus @@ -1983,8 +1982,8 @@ let add_morphism_as_parameter atts m n : unit = (Declare.ParameterEntry (None,(instance,uctx),None)) in Classes.add_instance (Classes.mk_instance - (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst) + (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (GlobRef.ConstRef cst)); + declare_projection n instance_id (GlobRef.ConstRef cst) let add_morphism_interactive atts m n : Lemmas.t = warn_add_morphism_deprecated ?loc:m.CAst.loc (); @@ -1997,11 +1996,11 @@ let add_morphism_interactive atts m n : Lemmas.t = let kind = Decls.(IsDefinition Instance) in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in let hook { DeclareDef.Hook.S.dref; _ } = dref |> function - | Globnames.ConstRef cst -> + | GlobRef.ConstRef cst -> Classes.add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info - atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst) + atts.global (GlobRef.ConstRef cst)); + declare_projection n instance_id (GlobRef.ConstRef cst) | _ -> assert false in let hook = DeclareDef.Hook.make hook in diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 4e79bab28e..e64129d204 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -203,11 +203,11 @@ let id_of_name = function end | Const (cst,_) -> Label.to_id (Constant.label cst) | Construct (cstr,_) -> - let ref = Globnames.ConstructRef cstr in + let ref = GlobRef.ConstructRef cstr in let basename = Nametab.basename_of_global ref in basename | Ind (ind,_) -> - let ref = Globnames.IndRef ind in + let ref = GlobRef.IndRef ind in let basename = Nametab.basename_of_global ref in basename | Sort s -> @@ -290,7 +290,7 @@ let coerce_to_evaluable_ref env sigma v = if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id else fail () else if has_type v (topwit wit_ref) then - let open Globnames in + let open GlobRef in let r = out_gen (topwit wit_ref) v in match r with | VarRef var -> EvalVarRef var diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 3ed5b1aab2..63559cf488 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -18,7 +18,6 @@ open Tacred open Util open Names open Libnames -open Globnames open Smartlocate open Constrexpr open Termops @@ -304,7 +303,7 @@ let intern_evaluable_reference_or_by_notation ist = function | {v=ByNotation (ntn,sc);loc} -> evaluable_of_global_reference ist.genv (Notation.interp_notation_as_global_reference ?loc - (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) + GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) (* Globalize a reduction expression *) let intern_evaluable ist r = @@ -383,7 +382,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = | GRef (r,None) -> Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) | GVar id -> - let r = evaluable_of_global_reference ist.genv (VarRef id) in + let r = evaluable_of_global_reference ist.genv (GlobRef.VarRef id) in Inl (ArgArg (r,None)) | _ -> let bound_names = Glob_ops.bound_glob_vars c in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 8ddf17ca14..c252372f21 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -22,7 +22,6 @@ open Util open Names open Nameops open Libnames -open Globnames open Refiner open Tacmach.New open Tactic_debug @@ -369,14 +368,14 @@ let interp_reference ist env sigma = function try try_interp_ltac_var (coerce_to_reference sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try - VarRef (get_id (Environ.lookup_named id env)) + GlobRef.VarRef (get_id (Environ.lookup_named id env)) with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in match v with | LocalDef _ -> EvalVarRef id - | _ -> error_not_evaluable (VarRef id) + | _ -> error_not_evaluable (GlobRef.VarRef id) let interp_evaluable ist env sigma = function | ArgArg (r,Some {loc;v=id}) -> diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 6aec83318c..3b79a130f2 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -27,7 +27,6 @@ open Tacmach.New open Tactics open Logic open Libnames -open Globnames open Nametab open Contradiction open Tactypes @@ -426,11 +425,11 @@ let destructurate_prop sigma t = | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args) | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args) | Const (sp,_), args -> - Kapp (Other (string_of_path (path_of_global (ConstRef sp))),args) + Kapp (Other (string_of_path (path_of_global (GlobRef.ConstRef sp))),args) | Construct (csp,_) , args -> - Kapp (Other (string_of_path (path_of_global (ConstructRef csp))), args) + Kapp (Other (string_of_path (path_of_global (GlobRef.ConstructRef csp))), args) | Ind (isp,_), args -> - Kapp (Other (string_of_path (path_of_global (IndRef isp))),args) + Kapp (Other (string_of_path (path_of_global (GlobRef.IndRef isp))),args) | Var id,[] -> Kvar id | Prod ({binder_name=Anonymous},typ,body), [] -> Kimp(typ,body) | Prod ({binder_name=Name _},_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal") diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 9973f2ec1d..eb75fca0a1 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -49,7 +49,7 @@ let global_head_of_constr sigma c = let global_of_constr_nofail c = try global_of_constr c - with Not_found -> VarRef (Id.of_string "dummy") + with Not_found -> GlobRef.VarRef (Id.of_string "dummy") let rec mk_clos_but f_map n t = let (f, args) = Constr.decompose_appvect t in diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index f0ae90beca..ca92d70263 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -12,7 +12,6 @@ open Printer open Pretyping -open Globnames open Glob_term open Tacmach @@ -47,7 +46,7 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) = let loc = rc.CAst.loc in match DAst.get rc with | GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' - | GRef (VarRef id, _) when not_section_id id -> + | GRef (Names.GlobRef.VarRef id, _) when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' | _ -> clr', rcs' @@ -89,7 +88,7 @@ let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c) let apply_rconstr ?ist t gl = (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *) let n = match ist, DAst.get t with - | None, (GVar id | GRef (VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id) + | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id) | Some ist, _ -> interp_nbargs ist gl t | _ -> anomaly "apply_rconstr without ist and not RVar" in let mkRlemma i = mkRApp t (mkRHoles i) in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 4c95a92022..33e9f871fd 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -181,7 +181,6 @@ let option_assert_get o msg = (** Constructors for rawconstr *) open Glob_term -open Globnames open Decl_kinds let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) @@ -191,14 +190,14 @@ let rec isRHoles cl = match cl with | [] -> true | c :: l -> match DAst.get c with GHole _ -> isRHoles l | _ -> false let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) -let mkRVar id = DAst.make @@ GRef (VarRef id,None) +let mkRVar id = DAst.make @@ GRef (GlobRef.VarRef id,None) let mkRltacVar id = DAst.make @@ GVar (id) let mkRCast rc rt = DAst.make @@ GCast (rc, CastConv rt) let mkRType = DAst.make @@ GSort (UAnonymous {rigid=true}) let mkRProp = DAst.make @@ GSort (UNamed [GProp,0]) let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2) -let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None) -let mkRInd mind = DAst.make @@ GRef (IndRef mind,None) +let mkRConstruct c = DAst.make @@ GRef (GlobRef.ConstructRef c,None) +let mkRInd mind = DAst.make @@ GRef (GlobRef.IndRef mind,None) let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t) let rec mkRnat n = @@ -1543,9 +1542,9 @@ let get g = end let is_construct_ref sigma c r = - EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r -let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r + EConstr.isConstruct sigma c && GlobRef.equal (GlobRef.ConstructRef (fst(EConstr.destConstruct sigma c))) r +let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (GlobRef.IndRef (fst(EConstr.destInd sigma c))) r let is_const_ref sigma c r = - EConstr.isConst sigma c && GlobRef.equal (ConstRef (fst(EConstr.destConst sigma c))) r + EConstr.isConst sigma c && GlobRef.equal (GlobRef.ConstRef (fst(EConstr.destConst sigma c))) r (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 7fc1a12b61..17db25660f 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -361,7 +361,7 @@ type tpattern = { let all_ok _ _ = true let proj_nparams c = - try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0 + try 1 + Recordops.find_projection_nparams (GlobRef.ConstRef c) with _ -> 0 let isRigid c = match kind c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true @@ -454,7 +454,7 @@ let ungen_upat lhs (sigma, uc, t) u = let nb_cs_proj_args pc f u = let na k = - List.length (snd (lookup_canonical_conversion (ConstRef pc, k))).o_TCOMPS in + List.length (snd (lookup_canonical_conversion (GlobRef.ConstRef pc, k))).o_TCOMPS in let nargs_of_proj t = match kind t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be @@ -928,7 +928,7 @@ let id_of_cpattern (_, (c1, c2), _) = Some (qualid_basename qid) | _, Some { v = CAppExpl ((_, qid, _), []) } when qualid_is_ident qid -> Some (qualid_basename qid) - | GRef (VarRef x, _), None -> Some x + | GRef (GlobRef.VarRef x, _), None -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with | Some x -> x @@ -1267,7 +1267,7 @@ let pf_fill_occ_term gl occ t = cl, t let cpattern_of_id id = - ' ', (DAst.make @@ GRef (VarRef id, None), None), Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty }) + ' ', (DAst.make @@ GRef (GlobRef.VarRef id, None), None), Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty }) let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with | _, Some { CAst.v = CHole _ } | GHole _, None -> true diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 0a1cc8745d..a148a3bc73 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -12,7 +12,6 @@ open Pp open Util open Names open Libnames -open Globnames open Constrexpr open Constrexpr_ops open Notation @@ -31,7 +30,7 @@ let get_constructors ind = let mib,oib = Global.lookup_inductive ind in let mc = oib.Declarations.mind_consnames in Array.to_list - (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) + (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc) let qualid_of_ref n = n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty @@ -40,7 +39,7 @@ let q_option () = qualid_of_ref "core.option.type" let unsafe_locate_ind q = match Nametab.locate q with - | IndRef i -> i + | GlobRef.IndRef i -> i | _ -> raise Not_found let locate_z () = @@ -166,7 +165,7 @@ let vernac_numeral_notation local ty f g scope opts = { pt_local = local; pt_scope = scope; pt_interp_info = NumeralNotation o; - pt_required = Nametab.path_of_global (IndRef tyc),[]; + pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; pt_refs = constructors; pt_in_match = true } in diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 1cbc86b6fe..649b51cb0e 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -10,7 +10,6 @@ open Util open Names -open Globnames open Glob_term open Bigint open Constrexpr @@ -40,9 +39,9 @@ let positive_kn = MutInd.make2 positive_modpath (Label.make "positive") let path_of_xI = ((positive_kn,0),1) let path_of_xO = ((positive_kn,0),2) let path_of_xH = ((positive_kn,0),3) -let glob_xI = ConstructRef path_of_xI -let glob_xO = ConstructRef path_of_xO -let glob_xH = ConstructRef path_of_xH +let glob_xI = GlobRef.ConstructRef path_of_xI +let glob_xO = GlobRef.ConstructRef path_of_xO +let glob_xH = GlobRef.ConstructRef path_of_xH let pos_of_bignat ?loc x = let ref_xI = DAst.make @@ GRef (glob_xI, None) in @@ -74,9 +73,9 @@ let z_kn = MutInd.make2 positive_modpath (Label.make "Z") let path_of_ZERO = ((z_kn,0),1) let path_of_POS = ((z_kn,0),2) let path_of_NEG = ((z_kn,0),3) -let glob_ZERO = ConstructRef path_of_ZERO -let glob_POS = ConstructRef path_of_POS -let glob_NEG = ConstructRef path_of_NEG +let glob_ZERO = GlobRef.ConstructRef path_of_ZERO +let glob_POS = GlobRef.ConstructRef path_of_POS +let glob_NEG = GlobRef.ConstructRef path_of_NEG let z_of_int ?loc n = if not (Bigint.equal n zero) then @@ -104,14 +103,14 @@ let rdefinitions = ["Coq";"Reals";"Rdefinitions"] let r_modpath = MPfile (make_dir rdefinitions) let r_path = make_path rdefinitions "R" -let glob_IZR = ConstRef (Constant.make2 r_modpath @@ Label.make "IZR") -let glob_Rmult = ConstRef (Constant.make2 r_modpath @@ Label.make "Rmult") -let glob_Rdiv = ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv") +let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR") +let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rmult") +let glob_Rdiv = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv") let binintdef = ["Coq";"ZArith";"BinIntDef"] let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z") -let glob_pow_pos = ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos") +let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos") let r_of_rawnum ?loc (sign,n) = let n, f, e = NumTok.(n.int, n.frac, n.exp) in diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index bc586acce7..8c0f9a3339 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -12,7 +12,6 @@ open Pp open Util open Names open Libnames -open Globnames open Constrexpr open Constrexpr_ops open Notation @@ -23,7 +22,7 @@ let get_constructors ind = let mib,oib = Global.lookup_inductive ind in let mc = oib.Declarations.mind_consnames in Array.to_list - (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) + (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc) let qualid_of_ref n = n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty @@ -92,7 +91,7 @@ let vernac_string_notation local ty f g scope = { pt_local = local; pt_scope = scope; pt_interp_info = StringNotation o; - pt_required = Nametab.path_of_global (IndRef tyc),[]; + pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; pt_refs = constructors; pt_in_match = true } in diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 47916ffb79..534c0ca20b 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -91,23 +91,23 @@ let rename_type ty ref = let rename_type_of_constant env c = let ty = Typeops.type_of_constant_in env c in - rename_type ty (ConstRef (fst c)) + rename_type ty (GlobRef.ConstRef (fst c)) let rename_type_of_inductive env ind = let ty = Inductiveops.type_of_inductive env ind in - rename_type ty (IndRef (fst ind)) + rename_type ty (GlobRef.IndRef (fst ind)) let rename_type_of_constructor env cstruct = let ty = Inductiveops.type_of_constructor env cstruct in - rename_type ty (ConstructRef (fst cstruct)) + rename_type ty (GlobRef.ConstructRef (fst cstruct)) let rename_typing env c = let j = Typeops.infer env c in let j' = match kind c with - | Const (c,u) -> { j with uj_type = rename_type j.uj_type (ConstRef c) } - | Ind (i,u) -> { j with uj_type = rename_type j.uj_type (IndRef i) } - | Construct (k,u) -> { j with uj_type = rename_type j.uj_type (ConstructRef k) } + | Const (c,u) -> { j with uj_type = rename_type j.uj_type (GlobRef.ConstRef c) } + | Ind (i,u) -> { j with uj_type = rename_type j.uj_type (GlobRef.IndRef i) } + | Construct (k,u) -> { j with uj_type = rename_type j.uj_type (GlobRef.ConstructRef k) } | _ -> j in j' diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 20dec96ef4..a562204b54 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -367,7 +367,7 @@ let make_return_predicate_ltac_lvar env sigma na tm c = - if [c] is a variable [id'], then [x] should now become [id'] - otherwise, [x] should be hidden *) match na, DAst.get tm with - | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' -> + | Name id, (GVar id' | GRef (GlobRef.VarRef id', _)) when Id.equal id id' -> let expansion = match kind sigma c with | Var id' -> Name id' | _ -> Anonymous in diff --git a/pretyping/classops.ml b/pretyping/classops.ml index afb546b2d2..1e5c07c061 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -225,14 +225,14 @@ let string_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" | CL_CONST sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp)) | CL_PROJ sp -> let sp = Projection.Repr.constant sp in - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp)) | CL_IND sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (IndRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.IndRef sp)) | CL_SECVAR sp -> - string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (VarRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.VarRef sp)) let pr_class x = str (string_of_class x) @@ -276,8 +276,8 @@ let lookup_path_to_fun_from env sigma s = let lookup_path_to_sort_from env sigma s = apply_on_class_of env sigma s lookup_path_to_sort_from_class -let mkNamed = function - | GlobRef.ConstRef c -> EConstr.mkConst c +let mkNamed = let open GlobRef in function + | ConstRef c -> EConstr.mkConst c | VarRef v -> EConstr.mkVar v | ConstructRef c -> EConstr.mkConstruct c | IndRef i -> EConstr.mkInd i @@ -325,8 +325,8 @@ let different_class_params env i = if (snd ci).cl_param > 0 then true else match fst ci with - | CL_IND i -> Environ.is_polymorphic env (IndRef i) - | CL_CONST c -> Environ.is_polymorphic env (ConstRef c) + | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i) + | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c) | _ -> false let add_coercion_in_graph env sigma (ic,source,target) = @@ -393,15 +393,15 @@ let reference_arity_length env sigma ref = List.length (fst (Reductionops.splay_arity env sigma (EConstr.of_constr t))) let projection_arity_length env sigma p = - let len = reference_arity_length env sigma (ConstRef (Projection.Repr.constant p)) in + let len = reference_arity_length env sigma (GlobRef.ConstRef (Projection.Repr.constant p)) in len - Projection.Repr.npars p let class_params env sigma = function | CL_FUN | CL_SORT -> 0 - | CL_CONST sp -> reference_arity_length env sigma (ConstRef sp) + | CL_CONST sp -> reference_arity_length env sigma (GlobRef.ConstRef sp) | CL_PROJ sp -> projection_arity_length env sigma sp - | CL_SECVAR sp -> reference_arity_length env sigma (VarRef sp) - | CL_IND sp -> reference_arity_length env sigma (IndRef sp) + | CL_SECVAR sp -> reference_arity_length env sigma (GlobRef.VarRef sp) + | CL_IND sp -> reference_arity_length env sigma (GlobRef.IndRef sp) (* add_class : cl_typ -> locality_flag option -> bool -> unit *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 415b9ec6df..e85c888b2e 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -15,7 +15,6 @@ open Util open Names open Constr open Context -open Globnames open Termops open EConstr open Vars @@ -237,11 +236,12 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = else raise PatternMatchingFailure in constrain sigma n c subst - + let matches_core env sigma allow_bound_rels (binding_vars,pat) c = let open EConstr in - let convref ref c = + let convref ref c = + let open GlobRef in match ref, EConstr.kind sigma c with | VarRef id, Var id' -> Names.Id.equal id id' | ConstRef c, Const (c',_) -> Constant.equal c c' @@ -270,7 +270,7 @@ let matches_core env sigma allow_bound_rels | PMeta None, m -> subst - | PRef (VarRef v1), Var v2 when Id.equal v1 v2 -> subst + | PRef (GlobRef.VarRef v1), Var v2 when Id.equal v1 v2 -> subst | PVar v1, Var v2 when Id.equal v1 v2 -> subst @@ -307,7 +307,7 @@ let matches_core env sigma allow_bound_rels | PApp (c1,arg1), App (c2,arg2) -> (match c1, EConstr.kind sigma c2 with - | PRef (ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr)) + | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr)) || Projection.unfolded pr -> raise PatternMatchingFailure | PProj (pr1,c1), Proj (pr,c) -> @@ -323,7 +323,7 @@ let matches_core env sigma allow_bound_rels try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure) - | PApp (PRef (ConstRef c1), _), Proj (pr, c2) + | PApp (PRef (GlobRef.ConstRef c1), _), Proj (pr, c2) when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) -> raise PatternMatchingFailure diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0daf1ab531..2061b41292 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -185,7 +185,7 @@ module PrintingInductiveMake = module Set = Indset let encode = Test.encode let subst subst obj = subst_ind subst obj - let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) + let printer ind = Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind) let key = ["Printing";Test.field] let title = Test.title let member_message x = Test.member_message (printer x) @@ -746,7 +746,7 @@ and detype_r d flags avoid env sigma t = GEvar (Id.of_string_soft ("M" ^ string_of_int n), []) | Var id -> (* Discriminate between section variable and non-section variable *) - (try let _ = Global.lookup_named id in GRef (VarRef id, None) + (try let _ = Global.lookup_named id in GRef (GlobRef.VarRef id, None) with Not_found -> GVar id) | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s)) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> @@ -772,20 +772,20 @@ and detype_r d flags avoid env sigma t = in mkapp (detype d flags avoid env sigma f) (Array.map_to_list (detype d flags avoid env sigma) args) - | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u) + | Const (sp,u) -> GRef (GlobRef.ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = let pars = Projection.npars p in let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Namegen.IntroAnonymous,None) in let args = List.make pars hole in - GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), + GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p), None), (args @ [detype d flags avoid env sigma c])) in if flags.flg_lax || !Flags.in_debugger || !Flags.in_toplevel then try noparams () with _ -> (* lax mode, used by debug printers only *) - GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), + GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p), None), [detype d flags avoid env sigma c]) else if print_primproj_params () then @@ -821,9 +821,9 @@ and detype_r d flags avoid env sigma t = GEvar (id, List.map (on_snd (detype d flags avoid env sigma)) l) | Ind (ind_sp,u) -> - GRef (IndRef ind_sp, detype_instance sigma u) + GRef (GlobRef.IndRef ind_sp, detype_instance sigma u) | Construct (cstr_sp,u) -> - GRef (ConstructRef cstr_sp, detype_instance sigma u) + GRef (GlobRef.ConstructRef cstr_sp, detype_instance sigma u) | Case (ci,p,c,bl) -> let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in detype_case comp (detype d flags avoid env sigma) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index edc948eb65..a82eff9cf0 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -263,7 +263,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = lookup_canonical_conversion (proji, Sort_cs (Sorts.family s)),[] | Proj (p, c) -> - let c2 = Globnames.ConstRef (Projection.constant p) in + let c2 = GlobRef.ConstRef (Projection.constant p) in let c = Retyping.expand_projection env sigma p c [] in let _, args = destApp sigma c in let sk2 = Stack.append_app args sk2 in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index ea94305dd8..6bde3dfd81 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -12,7 +12,6 @@ open Util open CAst open Names open Nameops -open Globnames open Glob_term open Evar_kinds @@ -443,7 +442,7 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function | GVar id as r -> let id' = rename_var l id in if id == id' then r else GVar id' - | GRef (VarRef id,_) as r -> + | GRef (GlobRef.VarRef id,_) as r -> if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming else r | GProd (na,bk,t,c) -> @@ -502,10 +501,10 @@ let rec cases_pattern_of_glob_constr env na c = | Anonymous -> PatVar (Name id) end | GHole (_,_,_) -> PatVar na - | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na) + | GRef (GlobRef.ConstructRef cstr,_) -> PatCstr (cstr,[],na) | GApp (c, l) -> begin match DAst.get c with - | GRef (ConstructRef cstr,_) -> + | GRef (GlobRef.ConstructRef cstr,_) -> let nparams = Inductiveops.inductive_nparams env (fst cstr) in let _,l = List.chop nparams l in PatCstr (cstr,List.map (cases_pattern_of_glob_constr env Anonymous) l,na) @@ -554,9 +553,9 @@ let add_alias ?loc na c = (* Turn a closed cases pattern into a glob_constr *) let rec glob_constr_of_cases_pattern_aux env isclosed x = DAst.map_with_loc (fun ?loc -> function - | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None)) + | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (GlobRef.ConstructRef cstr,None)) | PatCstr (cstr,l,na) -> - let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in + let ref = DAst.make ?loc @@ GRef (GlobRef.ConstructRef cstr,None) in let l = add_patterns_for_params_remove_local_defs env cstr l in add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux env isclosed) l)) | PatVar (Name id) when not isclosed -> diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index e25ebad380..a43549f6c3 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -17,7 +17,6 @@ open CErrors open Util open Names open Libnames -open Globnames open Nameops open Term open Constr @@ -624,7 +623,7 @@ let lookup_eliminator env ind_sp s = try let cst = Constant.make knu knc in let _ = lookup_constant cst env in - ConstRef cst + GlobRef.ConstRef cst with Not_found -> (* Then try to get a user-defined eliminator in some other places *) (* using short name (e.g. for "eq_rec") *) @@ -633,6 +632,6 @@ let lookup_eliminator env ind_sp s = user_err ~hdr:"default_elim" (strbrk "Cannot find the elimination combinator " ++ Id.print id ++ strbrk ", the elimination of the inductive definition " ++ - Nametab.pr_global_env Id.Set.empty (IndRef ind_sp) ++ + Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind_sp) ++ strbrk " on sort " ++ Sorts.pr_sort_family s ++ strbrk " is probably not allowed.") diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 3600f1761b..99e3c5025e 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -132,7 +132,7 @@ let rec head_pattern_bound t = | PIf (c,_,_) -> head_pattern_bound c | PCase (_,p,c,br) -> head_pattern_bound c | PRef r -> r - | PVar id -> VarRef id + | PVar id -> GlobRef.VarRef id | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ | PProj _ -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) @@ -140,10 +140,10 @@ let rec head_pattern_bound t = | PCoFix _ | PInt _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") let head_of_constr_reference sigma c = match EConstr.kind sigma c with - | Const (sp,_) -> ConstRef sp - | Construct (sp,_) -> ConstructRef sp - | Ind (sp,_) -> IndRef sp - | Var id -> VarRef id + | Const (sp,_) -> GlobRef.ConstRef sp + | Construct (sp,_) -> GlobRef.ConstructRef sp + | Ind (sp,_) -> GlobRef.IndRef sp + | Var id -> GlobRef.VarRef id | _ -> anomaly (Pp.str "Not a rigid reference.") let pattern_of_constr env sigma t = @@ -175,9 +175,9 @@ let pattern_of_constr env sigma t = with | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) - | Const (sp,u) -> PRef (ConstRef (Constant.make1 (Constant.canonical sp))) - | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) - | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) + | Const (sp,u) -> PRef (GlobRef.ConstRef (Constant.make1 (Constant.canonical sp))) + | Ind (sp,u) -> PRef (canonical_gr (GlobRef.IndRef sp)) + | Construct (sp,u) -> PRef (canonical_gr (GlobRef.ConstructRef sp)) | Proj (p, c) -> pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) [])) | Evar (evk,ctxt as ev) -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 280b6f9dae..c28c3ab730 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -37,7 +37,6 @@ open Vars open Reductionops open Type_errors open Typing -open Globnames open Evarutil open Evardefine open Pretype_errors @@ -435,7 +434,7 @@ let pretype_global ?loc rigid env evd gr us = let pretype_ref ?loc sigma env ref us = match ref with - | VarRef id -> + | GlobRef.VarRef id -> (* Section variable *) (try sigma, make_judge (mkVar id) (NamedDecl.get_type (lookup_named id !!env)) with Not_found -> diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 1b70119f20..48838a44c4 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -89,11 +89,11 @@ let lookup_structure indsp = Indmap.find indsp !structure_table let lookup_projections indsp = (lookup_structure indsp).s_PROJ let find_projection_nparams = function - | ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM + | GlobRef.ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM | _ -> raise Not_found let find_projection = function - | ConstRef cst -> Cmap.find cst !projection_table + | GlobRef.ConstRef cst -> Cmap.find cst !projection_table | _ -> raise Not_found let is_projection cst = Cmap.mem cst !projection_table @@ -185,7 +185,7 @@ let rec cs_pattern_of_constr env t = | Proj (p, c) -> let { Environ.uj_type = ty } = Typeops.infer env c in let _, params = Inductive.find_rectype env ty in - Const_cs (ConstRef (Projection.constant p)), None, params @ [c] + Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> Const_cs (global_of_constr t) , None, [] @@ -193,8 +193,8 @@ let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" (fun (sign,env,t,con,proji_sp) -> let env = Termops.push_rels_assum sign env in - let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in - let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in + let con_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef con) in + let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in strbrk "Projection value has no head constant: " ++ term_pp ++ strbrk " in canonical instance " @@ -223,7 +223,7 @@ let compute_canonical_projections env ~warn (con,ind) = Option.cata (fun proji_sp -> match cs_pattern_of_constr nenv t with | patt, o_INJ, o_TCOMPS -> - ((ConstRef proji_sp, (patt, t)), + ((GlobRef.ConstRef proji_sp, (patt, t)), { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) :: acc | exception Not_found -> @@ -281,7 +281,7 @@ let error_not_structure ref description = let check_and_decompose_canonical_structure env sigma ref = let sp = match ref with - ConstRef sp -> sp + GlobRef.ConstRef sp -> sp | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in let u = Univ.make_abstract_instance (Environ.constant_context env sp) in @@ -313,13 +313,13 @@ let lookup_canonical_conversion (proj,pat) = let decompose_projection sigma c args = match EConstr.kind sigma c with | Const (c, u) -> - let n = find_projection_nparams (ConstRef c) in + let n = find_projection_nparams (GlobRef.ConstRef c) in (* Check if there is some canonical projection attached to this structure *) - let _ = GlobRef.Map.find (ConstRef c) !object_table in + let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in let arg = Stack.nth args n in arg | Proj (p, c) -> - let _ = GlobRef.Map.find (ConstRef (Projection.constant p)) !object_table in + let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in c | _ -> raise Not_found diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d8f01c6bb5..7362955eb7 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -130,7 +130,7 @@ module ReductionBehaviour = struct | _ -> None let rebuild = function - | req, (ConstRef c, _ as x) -> req, x + | req, (GlobRef.ConstRef c, _ as x) -> req, x | _ -> assert false let inRedBehaviour = declare_object { @@ -958,7 +958,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) (body, stack) else (* Looks for ReductionBehaviour *) - match ReductionBehaviour.get (Globnames.ConstRef c) with + match ReductionBehaviour.get (GlobRef.ConstRef c) with | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) | Some behavior -> begin match behavior with @@ -1009,7 +1009,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = if not tactic_mode then let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in whrec Cst_stack.empty stack' - else match ReductionBehaviour.get (Globnames.ConstRef (Projection.constant p)) with + else match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with | None -> let stack' = (c, Stack.Proj (p, cst_l) :: stack) in let stack'', csts = whrec Cst_stack.empty stack' in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 6646dfb80c..6fdceb929a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -67,13 +67,13 @@ let value_of_evaluable_ref env evref u = | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get let evaluable_of_global_reference env = function - | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst - | VarRef id when is_evaluable_var env id -> EvalVarRef id + | GlobRef.ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst + | GlobRef.VarRef id when is_evaluable_var env id -> EvalVarRef id | r -> error_not_evaluable r let global_of_evaluable_reference = function - | EvalConstRef cst -> ConstRef cst - | EvalVarRef id -> VarRef id + | EvalConstRef cst -> GlobRef.ConstRef cst + | EvalVarRef id -> GlobRef.VarRef id type evaluable_reference = | EvalConst of Constant.t @@ -597,7 +597,7 @@ let special_red_case env sigma whfun (ci, p, c, lf) = let recargs = function | EvalVar _ | EvalRel _ | EvalEvar _ -> None - | EvalConst c -> ReductionBehaviour.get (ConstRef c) + | EvalConst c -> ReductionBehaviour.get (GlobRef.ConstRef c) let reduce_projection env sigma p ~npars (recarg'hd,stack') stack = (match EConstr.kind sigma recarg'hd with @@ -786,7 +786,7 @@ and whd_simpl_stack env sigma = let unf = Projection.unfolded p in if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then let npars = Projection.npars p in - (match unf, get (ConstRef (Projection.constant p)) with + (match unf, get (GlobRef.ConstRef (Projection.constant p)) with | false, Some NeverUnfold -> s' | false, Some (UnfoldWhen { recargs } | UnfoldWhenNoMatch { recargs }) when not (List.is_empty recargs) -> @@ -1101,7 +1101,7 @@ let string_of_evaluable_ref env = function | EvalVarRef id -> Id.to_string id | EvalConstRef kn -> string_of_qualid - (Nametab.shortest_qualid_of_global (vars_of_env env) (ConstRef kn)) + (Nametab.shortest_qualid_of_global (vars_of_env env) (GlobRef.ConstRef kn)) let unfold env sigma name c = if is_evaluable env name then @@ -1285,7 +1285,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = if isIndRef ref then let ((mind,u),t) = reduce_to_ind_gen allow_product env sigma t in begin match ref with - | IndRef mind' when eq_ind mind mind' -> t + | GlobRef.IndRef mind' when eq_ind mind mind' -> t | _ -> error_cannot_recognize ref end else diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 1d3e77452f..544fd3d17d 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -205,7 +205,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = | Some p, None -> Some (p + 1) | _, _ -> None in - Some (ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs + Some (GlobRef.ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs in let declare_proj hints (cref, info, body) = let path' = cref :: path in @@ -243,11 +243,11 @@ let instance_constructor (cl,u) args = let open EConstr in let pars = fst (List.chop lenpars args) in match cl.cl_impl with - | IndRef ind -> + | GlobRef.IndRef ind -> let ind = ind, u in (Some (applist (mkConstructUi (ind, 1), args)), applist (mkIndU ind, pars)) - | ConstRef cst -> + | GlobRef.ConstRef cst -> let cst = cst, u in let term = match args with | [] -> None diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9b1acddef1..5e57a26d8e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -68,7 +68,7 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n (*******************) (** Basic printing *) -let print_basename sp = pr_global (ConstRef sp) +let print_basename sp = pr_global (GlobRef.ConstRef sp) let print_ref reduce ref udecl = let env = Global.env () in @@ -82,7 +82,7 @@ let print_ref reduce ref udecl = let ctx,ccl = Reductionops.splay_prod_assum env sigma typ in EConstr.it_mkProd_or_LetIn ccl ctx else typ in - let variance = match ref with + let variance = let open GlobRef in match ref with | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> let mind = Environ.lookup_mind ind env in @@ -184,10 +184,10 @@ type opacity = let opacity env = function - | VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) -> + | GlobRef.VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) -> Some(TransparentMaybeOpacified (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) - | ConstRef cst -> + | GlobRef.ConstRef cst -> let cb = Environ.lookup_constant cst env in (match cb.const_body with | Undef _ | Primitive _ -> None @@ -247,7 +247,7 @@ let print_primitive_record recflag mipv = function let print_primitive ref = match ref with - | IndRef ind -> + | GlobRef.IndRef ind -> let mib,_ = Global.lookup_inductive ind in print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record | _ -> [] @@ -281,10 +281,10 @@ let print_id_args_data test pr id l = let print_args_data_of_inductive_ids get test pr sp mipv = List.flatten (Array.to_list (Array.mapi (fun i mip -> - print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) @ + print_id_args_data test pr mip.mind_typename (get (GlobRef.IndRef (sp,i))) @ List.flatten (Array.to_list (Array.mapi (fun j idc -> - print_id_args_data test pr idc (get (ConstructRef ((sp,i),j+1)))) + print_id_args_data test pr idc (get (GlobRef.ConstructRef ((sp,i),j+1)))) mip.mind_consnames))) mipv)) @@ -358,7 +358,7 @@ let locate_any_name qid = let pr_located_qualid = function | Term ref -> - let ref_str = match ref with + let ref_str = let open GlobRef in match ref with ConstRef _ -> "Constant" | IndRef _ -> "Inductive" | ConstructRef _ -> "Constructor" @@ -382,7 +382,7 @@ let pr_located_qualid = function | Undefined qid -> pr_qualid qid ++ spc () ++ str "not a defined object." -let canonize_ref = function +let canonize_ref = let open GlobRef in function | ConstRef c -> let kn = Constant.canonical c in if KerName.equal (Constant.user c) kn then None @@ -537,7 +537,7 @@ let print_named_decl env sigma id = let gallina_print_section_variable env sigma id = print_named_decl env sigma id ++ - with_line_skip (print_name_infos (VarRef id)) + with_line_skip (print_name_infos (GlobRef.VarRef id)) let print_body env evd = function | Some c -> pr_lconstr_env env evd c @@ -595,7 +595,7 @@ let print_constant with_values sep sp udecl = let gallina_print_constant_with_infos sp udecl = print_constant true " = " sp udecl ++ - with_line_skip (print_name_infos (ConstRef sp)) + with_line_skip (print_name_infos (GlobRef.ConstRef sp)) let gallina_print_syntactic_def env kn = let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn @@ -786,6 +786,7 @@ let print_sec_context_typ env sigma sec = print_context env sigma false None (read_sec_context sec) let maybe_error_reject_univ_decl na udecl = + let open GlobRef in match na, udecl with | _, None | Term (ConstRef _ | IndRef _ | ConstructRef _), Some _ -> () | (Term (VarRef _) | Syntactic _ | Dir _ | ModuleType _ | Other _ | Undefined _), Some udecl -> @@ -794,6 +795,7 @@ let maybe_error_reject_univ_decl na udecl = let print_any_name env sigma na udecl = maybe_error_reject_univ_decl na udecl; + let open GlobRef in match na with | Term (ConstRef sp) -> print_constant_with_infos sp udecl | Term (IndRef (sp,_)) -> print_inductive sp udecl @@ -825,6 +827,7 @@ let print_name env sigma na udecl = print_any_name env sigma (locate_any_name ref) udecl let print_opaque_name env sigma qid = + let open GlobRef in match Nametab.global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in diff --git a/printing/printer.ml b/printing/printer.ml index 1f68018678..97b3233d12 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -15,7 +15,6 @@ open Names open Constr open Context open Environ -open Globnames open Evd open Refiner open Constrextern @@ -155,7 +154,7 @@ let pr_in_comment x = str "(* " ++ x ++ str " *)" the [mutual_inductive_body] for the inductives and constructors (needs an environment for this). *) -let id_of_global env = function +let id_of_global env = let open GlobRef in function | ConstRef kn -> Label.to_id (Constant.label kn) | IndRef (kn,0) -> Label.to_id (MutInd.label kn) | IndRef (kn,i) -> @@ -170,7 +169,7 @@ let rec dirpath_of_mp = function | MPdot (mp,l) -> Libnames.add_dirpath_suffix (dirpath_of_mp mp) (Label.to_id l) -let dirpath_of_global = function +let dirpath_of_global = let open GlobRef in function | ConstRef kn -> dirpath_of_mp (Constant.modpath kn) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> dirpath_of_mp (MutInd.modpath kn) @@ -251,7 +250,7 @@ let pr_puniverses f env sigma (c,u) = then f env c ++ pr_universe_instance sigma u else f env c -let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) +let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef cst) let pr_existential_key = Termops.pr_existential_key let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev) let pr_inductive env ind = pr_lconstr_env env (Evd.from_env env) (mkInd ind) diff --git a/printing/printmod.ml b/printing/printmod.ml index 74d4f69c9c..43992ec9d3 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -15,7 +15,6 @@ open Pp open Names open Environ open Declarations -open Globnames open Libnames open Goptions @@ -231,13 +230,13 @@ let nametab_register_body mp dir (l,body) = | SFBmodule _ -> () (* TODO *) | SFBmodtype _ -> () (* TODO *) | SFBconst _ -> - push (Label.to_id l) (ConstRef (Constant.make2 mp l)) + push (Label.to_id l) (GlobRef.ConstRef (Constant.make2 mp l)) | SFBmind mib -> let mind = MutInd.make2 mp l in Array.iteri (fun i mip -> - push mip.mind_typename (IndRef (mind,i)); - Array.iteri (fun j id -> push id (ConstructRef ((mind,i),j+1))) + push mip.mind_typename (GlobRef.IndRef (mind,i)); + Array.iteri (fun j id -> push id (GlobRef.ConstructRef ((mind,i),j+1))) mip.mind_consnames) mib.mind_packets diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index a476381b17..d74935721f 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -13,7 +13,6 @@ open Constr open EConstr open Names open Pattern -open Globnames (* Discrimination nets with bounded depth. See the module dn.ml for further explanations. @@ -36,7 +35,7 @@ type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything let decomp_pat = let rec decrec acc = function | PApp (f,args) -> decrec (Array.to_list args @ acc) f - | PProj (p, c) -> (PRef (ConstRef (Projection.constant p)), c :: acc) + | PProj (p, c) -> (PRef (GlobRef.ConstRef (Projection.constant p)), c :: acc) | c -> (c,acc) in decrec [] @@ -51,6 +50,7 @@ let decomp sigma t = decrec [] t let constr_val_discr sigma t = + let open GlobRef in let c, l = decomp sigma t in match EConstr.kind sigma c with | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l) @@ -63,6 +63,7 @@ let constr_pat_discr t = if not (Patternops.occur_meta_pattern t) then None else + let open GlobRef in match decomp_pat t with | PRef ((IndRef _) as ref), args | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) @@ -71,6 +72,7 @@ let constr_pat_discr t = let constr_val_discr_st sigma ts t = let c, l = decomp sigma t in + let open GlobRef in match EConstr.kind sigma c with | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l) | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l) @@ -86,6 +88,7 @@ let constr_val_discr_st sigma ts t = | _ -> Nothing let constr_pat_discr_st ts t = + let open GlobRef in match decomp_pat t with | PRef ((IndRef _) as ref), args | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 303ddacb67..ce06e656ed 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -25,7 +25,6 @@ open Tacmach open Tactics open Clenv open Typeclasses -open Globnames open Evd open Locus open Proofview.Notations @@ -517,8 +516,8 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = let rec iscl env ty = let ctx, ar = decompose_prod_assum sigma ty in match EConstr.kind sigma (fst (decompose_app sigma ar)) with - | Const (c,_) -> is_class (ConstRef c) - | Ind (i,_) -> is_class (IndRef i) + | Const (c,_) -> is_class (GlobRef.ConstRef c) + | Ind (i,_) -> is_class (GlobRef.IndRef i) | _ -> let env' = push_rel_context ctx env in let ty' = Reductionops.whd_all env' sigma ar in @@ -529,10 +528,10 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = let keep = not only_classes || is_class in if keep then let c = mkVar id in - let name = PathHints [VarRef id] in + let name = PathHints [GlobRef.VarRef id] in let hints = if is_class then - let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in + let hints = build_subclasses ~check:false env sigma (GlobRef.VarRef id) empty_hint_info in (List.map_append (fun (path,info,c) -> make_resolves env sigma ~name:(PathHints path) diff --git a/tactics/equality.ml b/tactics/equality.ml index 98db6cbb97..7c90c59f61 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -380,7 +380,7 @@ let find_elim hdcncl lft2rgt dep cls ot = Logic.eq or Jmeq just before *) assert false in - pf_constr_of_global (ConstRef c) + pf_constr_of_global (GlobRef.ConstRef c) else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) @@ -399,7 +399,7 @@ let find_elim hdcncl lft2rgt dep cls ot = let c, eff = find_scheme scheme_name ind in Proofview.tclEFFECTS eff <*> - pf_constr_of_global (ConstRef c) + pf_constr_of_global (GlobRef.ConstRef c) | _ -> assert false end @@ -989,7 +989,7 @@ let ind_scheme_of_eq lbeq to_kind = (* use ind rather than case by compatibility *) let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in let c, eff = find_scheme kind (destIndRef lbeq.eq) in - ConstRef c, eff + GlobRef.ConstRef c, eff let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = diff --git a/tactics/hints.ml b/tactics/hints.ml index 8d1c536db6..131832be89 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -48,6 +48,7 @@ let head_constr_bound sigma t = let t = strip_outer_cast sigma t in let _,ccl = decompose_prod_assum sigma t in let hd,args = decompose_app sigma ccl in + let open GlobRef in match EConstr.kind sigma hd with | Const (c, _) -> ConstRef c | Ind (i, _) -> IndRef i @@ -65,6 +66,7 @@ let decompose_app_bound sigma t = let t = strip_outer_cast sigma t in let _,ccl = decompose_prod_assum sigma t in let hd,args = decompose_app_vect sigma ccl in + let open GlobRef in match EConstr.kind sigma hd with | Const (c,u) -> ConstRef c, args | Ind (i,u) -> IndRef i, args @@ -295,7 +297,7 @@ let lookup_tacs sigma concl st se = let sl' = List.stable_sort pri_order_int l' in List.merge pri_order_int se.sentry_nopat sl' -let is_transparent_gr ts = function +let is_transparent_gr ts = let open GlobRef in function | VarRef id -> TransparentState.is_transparent_variable ts id | ConstRef cst -> TransparentState.is_transparent_constant ts cst | IndRef _ | ConstructRef _ -> false @@ -919,7 +921,7 @@ let make_resolve_hyp env sigma decl = let c = mkVar hname in try [make_apply_entry env sigma (true, true, false) empty_hint_info ~poly:false - ~name:(PathHints [VarRef hname]) + ~name:(PathHints [GlobRef.VarRef hname]) (c, NamedDecl.get_type decl, Univ.ContextSet.empty)] with | Failure _ -> [] @@ -1326,7 +1328,7 @@ let project_hint ~poly pri l2r r = ~name ~kind:Decls.(IsDefinition Definition) cb in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in - (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c)) + (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c)) let interp_hints ~poly = fun h -> @@ -1376,7 +1378,7 @@ let interp_hints ~poly = Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind"; List.init (nconstructors env ind) (fun i -> let c = (ind,i+1) in - let gr = ConstructRef c in + let gr = GlobRef.ConstructRef c in empty_hint_info, (Declareops.inductive_is_polymorphic mib), true, PathHints [gr], IsGlobRef gr) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9dabe56816..6fd18b83d1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -24,7 +24,6 @@ open Namegen open Declarations open Inductiveops open Reductionops -open Globnames open Evd open Tacred open Genredexpr @@ -921,14 +920,14 @@ let is_local_flag env flags = else let check = function | EvalVarRef _ -> false - | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c)) + | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (GlobRef.ConstRef c)) in List.for_all check flags.rConst let is_local_unfold env flags = let check (_, c) = match c with | EvalVarRef _ -> false - | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c)) + | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (GlobRef.ConstRef c)) in List.for_all check flags @@ -975,8 +974,8 @@ let reduce redexp cl = (* Unfolding occurrences of a constant *) let unfold_constr = function - | ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp] - | VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id] + | GlobRef.ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp] + | GlobRef.VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id] | _ -> user_err ~hdr:"unfold_constr" (str "Cannot unfold a non-constant.") (*******************************************) diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index c3132ed6f0..ccd7a818b9 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -289,6 +289,7 @@ struct open TDnet let pat_of_constr c : term_pattern = + let open GlobRef in (* To each evar we associate a unique identifier. *) let metas = ref Evar.Map.empty in let rec pat_of_constr c = match Constr.kind c with diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index a05612c1b1..f6775ddd1f 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1094,7 +1094,7 @@ let () = let () = let intern self ist ref = match ref.CAst.v with | Tac2qexpr.QHypothesis id -> - GlbVal (Globnames.VarRef id), gtypref t_reference + GlbVal (GlobRef.VarRef id), gtypref t_reference | Tac2qexpr.QReference qid -> let gr = try Nametab.locate qid @@ -1106,7 +1106,7 @@ let () = let subst s c = Globnames.subst_global_reference s c in let interp _ gr = return (Value.of_reference gr) in let print _ = function - | Globnames.VarRef id -> str "reference:(" ++ str "&" ++ Id.print id ++ str ")" + | GlobRef.VarRef id -> str "reference:(" ++ str "&" ++ Id.print id ++ str ")" | r -> str "reference:(" ++ Printer.pr_global r ++ str ")" in let obj = { diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml index ee61bdab71..0e6fb94095 100644 --- a/user-contrib/Ltac2/tac2ffi.ml +++ b/user-contrib/Ltac2/tac2ffi.ml @@ -10,7 +10,6 @@ open Util open Names -open Globnames open Tac2dyn open Tac2expr open Proofview.Notations @@ -337,13 +336,13 @@ let of_constant c = of_ext val_constant c let to_constant c = to_ext val_constant c let constant = repr_ext val_constant -let of_reference = function +let of_reference = let open GlobRef in function | VarRef id -> ValBlk (0, [| of_ident id |]) | ConstRef cst -> ValBlk (1, [| of_constant cst |]) | IndRef ind -> ValBlk (2, [| of_ext val_inductive ind |]) | ConstructRef cstr -> ValBlk (3, [| of_ext val_constructor cstr |]) -let to_reference = function +let to_reference = let open GlobRef in function | ValBlk (0, [| id |]) -> VarRef (to_ident id) | ValBlk (1, [| cst |]) -> ConstRef (to_constant cst) | ValBlk (2, [| ind |]) -> IndRef (to_ext val_inductive ind) diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml index 6c96ef7742..561bd9c0c5 100644 --- a/user-contrib/Ltac2/tac2tactics.ml +++ b/user-contrib/Ltac2/tac2tactics.ml @@ -11,7 +11,6 @@ open Pp open Util open Names -open Globnames open Tac2types open Tac2extffi open Genredexpr @@ -209,13 +208,13 @@ let letin_pat_tac ev ipat na c cl = Instead, we parse indifferently any pattern and dispatch when the tactic is called. *) let map_pattern_with_occs (pat, occ) = match pat with -| Pattern.PRef (ConstRef cst) -> (mk_occurrences_expr occ, Inl (EvalConstRef cst)) -| Pattern.PRef (VarRef id) -> (mk_occurrences_expr occ, Inl (EvalVarRef id)) +| Pattern.PRef (GlobRef.ConstRef cst) -> (mk_occurrences_expr occ, Inl (EvalConstRef cst)) +| Pattern.PRef (GlobRef.VarRef id) -> (mk_occurrences_expr occ, Inl (EvalVarRef id)) | _ -> (mk_occurrences_expr occ, Inr pat) let get_evaluable_reference = function -| VarRef id -> Proofview.tclUNIT (EvalVarRef id) -| ConstRef cst -> Proofview.tclUNIT (EvalConstRef cst) +| GlobRef.VarRef id -> Proofview.tclUNIT (EvalVarRef id) +| GlobRef.ConstRef cst -> Proofview.tclUNIT (EvalConstRef cst) | r -> Tacticals.New.tclZEROMSG (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ spc () ++ diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index d7cb9dc727..ab341e4ab8 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -24,7 +24,6 @@ open Constr open Context open Declarations open Mod_subst -open Globnames open Printer open Context.Named.Declaration @@ -157,13 +156,15 @@ let lookup_mind mind = (** Graph traversal of an object, collecting on the way the dependencies of traversed objects *) -let label_of = function +let label_of = let open GlobRef in function | ConstRef kn -> Constant.label kn | IndRef (kn,_) | ConstructRef ((kn,_),_) -> MutInd.label kn | VarRef id -> Label.of_id id -let rec traverse current ctx accu t = match Constr.kind t with +let rec traverse current ctx accu t = + let open GlobRef in + match Constr.kind t with | Var id -> let body () = id |> Global.lookup_named |> NamedDecl.get_value in traverse_object accu body (VarRef id) @@ -218,7 +219,7 @@ and traverse_object ?inhabits (curr, data, ax2ty) body obj = definition share exactly the same dependencies. Also, there is no explicit dependency between mutually defined inductives and constructors. *) and traverse_inductive (curr, data, ax2ty) mind obj = - let firstind_ref = (IndRef (mind, 0)) in + let firstind_ref = (GlobRef.IndRef (mind, 0)) in let label = label_of obj in let data, ax2ty = (* Invariant : I_0 \in data iff I_i \in data iff c_ij \in data @@ -264,9 +265,9 @@ and traverse_inductive (curr, data, ax2ty) mind obj = (* Maps all these dependencies to inductives and constructors*) let data = Array.fold_left_i (fun n data oib -> let ind = (mind, n) in - let data = GlobRef.Map_env.add (IndRef ind) contents data in + let data = GlobRef.Map_env.add (GlobRef.IndRef ind) contents data in Array.fold_left_i (fun k data _ -> - GlobRef.Map_env.add (ConstructRef (ind, k+1)) contents data + GlobRef.Map_env.add (GlobRef.ConstructRef (ind, k+1)) contents data ) data oib.mind_consnames) data mib.mind_packets in data, ax2ty @@ -298,6 +299,7 @@ let type_of_constant cb = cb.Declarations.const_type let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = (* Only keep the transitive dependencies *) let (_, graph, ax2ty) = traverse (label_of gr) t in + let open GlobRef in let fold obj _ accu = match obj with | VarRef id -> let decl = Global.lookup_named id in diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 9b96fbf68a..d414d57c0d 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -21,7 +21,6 @@ open Vars open Termops open Declarations open Names -open Globnames open Inductiveops open Tactics open Ind_tables @@ -201,7 +200,7 @@ let build_beq_scheme mode kn = let eid = Id.of_string ("eq_"^(Id.to_string x)) in let () = try ignore (Environ.lookup_named eid env) - with Not_found -> raise (ParameterWithoutEquality (VarRef x)) + with Not_found -> raise (ParameterWithoutEquality (GlobRef.VarRef x)) in mkVar eid, Evd.empty_side_effects | Cast (x,_,_) -> aux (Term.applist (x,a)) @@ -240,7 +239,7 @@ let build_beq_scheme mode kn = try let _ = Environ.constant_opt_value_in env (kneq, u) in Term.applist (mkConst kneq,a), Evd.empty_side_effects - with Not_found -> raise (ParameterWithoutEquality (ConstRef kn))) + with Not_found -> raise (ParameterWithoutEquality (GlobRef.ConstRef kn))) | Proj _ -> raise (EqUnknown "projection") | Construct _ -> raise (EqUnknown "constructor") | Case _ -> raise (EqUnknown "match") @@ -655,7 +654,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). | App (c,ca) -> ( match EConstr.kind sigma c with | Ind (indeq, u) -> - if GlobRef.equal (IndRef indeq) Coqlib.(lib_ref "core.eq.type") + if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type") then Tacticals.New.tclTHEN (do_replace_bl mode bl_scheme_key ind diff --git a/vernac/class.ml b/vernac/class.ml index f79e459f43..766625a21a 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -20,7 +20,6 @@ open Termops open Environ open Classops open Declare -open Globnames open Libobject let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL @@ -71,10 +70,10 @@ let check_reference_arity ref = let check_arity = function | CL_FUN | CL_SORT -> () - | CL_CONST cst -> check_reference_arity (ConstRef cst) - | CL_PROJ p -> check_reference_arity (ConstRef (Projection.Repr.constant p)) - | CL_SECVAR id -> check_reference_arity (VarRef id) - | CL_IND kn -> check_reference_arity (IndRef kn) + | CL_CONST cst -> check_reference_arity (GlobRef.ConstRef cst) + | CL_PROJ p -> check_reference_arity (GlobRef.ConstRef (Projection.Repr.constant p)) + | CL_SECVAR id -> check_reference_arity (GlobRef.VarRef id) + | CL_IND kn -> check_reference_arity (GlobRef.IndRef kn) (* Coercions *) @@ -90,12 +89,12 @@ let uniform_cond sigma ctx lt = lt (Context.Rel.to_extended_list EConstr.mkRel 0 ctx) let class_of_global = function - | ConstRef sp -> + | GlobRef.ConstRef sp -> (match Recordops.find_primitive_projection sp with | Some p -> CL_PROJ p | None -> CL_CONST sp) - | IndRef sp -> CL_IND sp - | VarRef id -> CL_SECVAR id - | ConstructRef _ as c -> + | GlobRef.IndRef sp -> CL_IND sp + | GlobRef.VarRef id -> CL_SECVAR id + | GlobRef.ConstructRef _ as c -> user_err ~hdr:"class_of_global" (str "Constructors, such as " ++ Printer.pr_global c ++ str ", cannot be used as a class.") @@ -152,7 +151,7 @@ let strength_of_cl = function | _ -> `GLOBAL let strength_of_global = function - | VarRef _ -> `LOCAL + | GlobRef.VarRef _ -> `LOCAL | _ -> `GLOBAL let get_strength stre ref cls clt = @@ -179,7 +178,7 @@ let build_id_coercion idf_opt source poly = let env = Global.env () in let sigma = Evd.from_env env in let sigma, vs = match source with - | CL_CONST sp -> Evd.fresh_global env sigma (ConstRef sp) + | CL_CONST sp -> Evd.fresh_global env sigma (GlobRef.ConstRef sp) | _ -> error_not_transparent source in let vs = EConstr.Unsafe.to_constr vs in let c = match constant_opt_value_in env (destConst vs) with @@ -223,7 +222,7 @@ let build_id_coercion idf_opt source poly = in let kind = Decls.(IsDefinition IdentityCoercion) in let kn = declare_constant ~name ~kind constr_entry in - ConstRef kn + GlobRef.ConstRef kn let check_source = function | Some (CL_FUN as s) -> raise (CoercionError (ForbiddenSourceClass s)) @@ -267,7 +266,7 @@ let inCoercion : coercion -> obj = let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps = let isproj = match coef with - | ConstRef c -> Recordops.find_primitive_projection c + | GlobRef.ConstRef c -> Recordops.find_primitive_projection c | _ -> None in let c = { diff --git a/vernac/classes.ml b/vernac/classes.ml index 24f4f7fe70..efe452d5f1 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -193,6 +193,7 @@ let discharge_class (_,cl) = ctx in let abs_context cl = + let open GlobRef in match cl.cl_impl with | VarRef _ | ConstructRef _ -> assert false | ConstRef cst -> Lib.section_segment_of_constant cst @@ -255,7 +256,7 @@ let add_class env sigma cl = | Some (Backward, info) -> (match body with | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") - | Some b -> declare_instance ~warn:true env sigma (Some info) false (ConstRef b)) + | Some b -> declare_instance ~warn:true env sigma (Some info) false (GlobRef.ConstRef b)) | _ -> ()) cl.cl_projs @@ -298,6 +299,7 @@ let type_ctx_instance ~program_mode env sigma ctx inst subst = in aux (sigma, subst, []) inst (List.rev ctx) let id_of_class cl = + let open GlobRef in match cl.cl_impl with | ConstRef kn -> Label.to_id @@ Constant.label kn | IndRef (kn,i) -> @@ -325,8 +327,8 @@ let declare_instance_constant info global imps ?hook name decl poly sigma term t let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in Declare.definition_message name; - Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); - instance_hook info global imps ?hook (ConstRef kn) + Declare.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); + instance_hook info global imps ?hook (GlobRef.ConstRef kn) let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name = let subst = List.fold_left2 @@ -338,17 +340,17 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst nam let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in - Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); - instance_hook pri global imps (ConstRef cst) + Declare.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); + instance_hook pri global imps (GlobRef.ConstRef cst) let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype = let hook { DeclareDef.Hook.S.scope; dref; _ } = - let cst = match dref with ConstRef kn -> kn | _ -> assert false in + let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false dref imps; let pri = intern_info pri in let env = Global.env () in let sigma = Evd.from_env env in - declare_instance env sigma (Some pri) (not global) (ConstRef cst) + declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst) in let obls, constr, typ = match term with @@ -440,7 +442,7 @@ let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = let {CAst.loc;v=mid} = get_id loc_mid in List.iter (fun (n, _, x) -> if Name.equal n (Name mid) then - Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs; + Option.iter (fun x -> Dumpglob.add_glob ?loc (GlobRef.ConstRef x)) x) k.cl_projs; c :: props, rest' with Not_found -> ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index c561d4a2a4..d59d471d5f 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -14,7 +14,6 @@ open Vars open Declare open Names open Context -open Globnames open Constrexpr_ops open Constrintern open Impargs @@ -54,7 +53,7 @@ match scope with let decl = SectionLocalAssum {typ; univs; poly; impl} in let () = declare_variable ~name ~kind decl in let () = assumption_message name in - let r = VarRef name in + let r = GlobRef.VarRef name in let () = maybe_declare_manual_implicits true r imps in let env = Global.env () in let sigma = Evd.from_env env in @@ -72,7 +71,7 @@ match scope with let kind = Decls.IsAssumption kind in let decl = Declare.ParameterEntry (None,(typ,univs),inl) in let kn = declare_constant ~name ~local ~kind decl in - let gr = ConstRef kn in + let gr = GlobRef.ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in let () = Declare.declare_univ_binders gr pl in let () = assumption_message name in @@ -285,7 +284,7 @@ let context ~poly l = in let cst = Declare.declare_constant ~name ~kind decl in let env = Global.env () in - Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst); + Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (GlobRef.ConstRef cst); status else let test x = match x.CAst.v with diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index d99d3e65fd..65db4401d9 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -18,7 +18,6 @@ open Environ open Declare open Names open Libnames -open Globnames open Nameops open Constrexpr open Constrexpr_ops @@ -522,7 +521,7 @@ let is_recursive mie = let warn_non_primitive_record = CWarnings.create ~name:"non-primitive-record" ~category:"record" (fun indsp -> - (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (IndRef indsp) ++ + (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++ strbrk" could not be defined as a primitive record"))) let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls = @@ -540,15 +539,15 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p let (_, kn), prim = declare_mind mie in let mind = Global.mind_of_delta_kn kn in if primitive_expected && not prim then warn_non_primitive_record (mind,0); - Declare.declare_univ_binders (IndRef (mind,0)) pl; + Declare.declare_univ_binders (GlobRef.IndRef (mind,0)) pl; List.iteri (fun i (indimpls, constrimpls) -> let ind = (mind,i) in - let gr = IndRef ind in + let gr = GlobRef.IndRef ind in maybe_declare_manual_implicits false gr indimpls; List.iteri (fun j impls -> maybe_declare_manual_implicits false - (ConstructRef (ind, succ j)) impls) + (GlobRef.ConstructRef (ind, succ j)) impls) constrimpls) impls; Flags.if_verbose Feedback.msg_info (minductive_message names); @@ -614,6 +613,6 @@ let make_cases ind = let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n.Context.binder_name avoid in Id.to_string n' :: rename (Id.Set.add n' avoid) l in let al' = rename Id.Set.empty al in - let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in + let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) mip.mind_nf_lc [] diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 4d663d6b0e..0fd65ad9b4 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -17,7 +17,6 @@ open Vars open Declare open Names open Libnames -open Globnames open Nameops open Constrexpr open Constrexpr_ops @@ -213,7 +212,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in (* FIXME: include locality *) let c = Declare.declare_constant ~name:recname ~kind:Decls.(IsDefinition Definition) (DefinitionEntry ce) in - let gr = ConstRef c in + let gr = GlobRef.ConstRef c in if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr impls in diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 69338c0ba6..5e4f2dcd34 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -9,7 +9,6 @@ (************************************************************************) open Declare -open Globnames open Impargs type locality = Discharge | Global of Declare.import_status @@ -51,10 +50,10 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let () = declare_variable ~name ~kind:Decls.(IsDefinition kind) (SectionLocalDef ce) in - VarRef name + Names.GlobRef.VarRef name | Global local -> let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in - let gr = ConstRef kn in + let gr = Names.GlobRef.ConstRef kn in let () = Declare.declare_univ_binders gr udecl in gr in diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index d9b839e857..23a8bf20a3 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -27,7 +27,6 @@ open Inductive open Indrec open Declare open Libnames -open Globnames open Goptions open Nameops open Termops @@ -376,7 +375,7 @@ requested | InSet -> recs ^ "_nodep" | InType -> recs ^ "t_nodep") ) in - let newid = add_suffix (Nametab.basename_of_global (IndRef ind)) suffix in + let newid = add_suffix (Nametab.basename_of_global (GlobRef.IndRef ind)) suffix in let newref = CAst.make newid in ((newref,isdep,ind,z)::l1),l2 in @@ -394,7 +393,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let evd, indu, inst = match inst with | None -> - let _, ctx = Typeops.type_of_global_in_context env0 (IndRef ind) in + let _, ctx = Typeops.type_of_global_in_context env0 (GlobRef.IndRef ind) in let u, ctx = UnivGen.fresh_instance_from ctx None in let evd = Evd.from_ctx (UState.of_context_set ctx) in evd, (ind,u), Some u @@ -408,14 +407,14 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = (* NB: build_mutual_induction_scheme forces nonempty list of mutual inductives (force_mutual is about the generated schemes) *) let _,_,ind,_ = List.hd lnamedepindsort in - Global.is_polymorphic (IndRef ind) + Global.is_polymorphic (GlobRef.IndRef ind) in let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let decltype = EConstr.to_constr sigma decltype in let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in let cst = define ~poly fi sigma proof_output (Some decltype) in - ConstRef cst :: lrecref + GlobRef.ConstRef cst :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in fixpoint_message None lrecnames @@ -542,7 +541,7 @@ let do_combined_scheme name schemes = polymorphism of the inductive block). In that case if they want some other polymorphism they can also manually define the combined scheme. *) - let poly = Global.is_polymorphic (ConstRef (List.hd csts)) in + let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in ignore (define ~poly name.v sigma proof_output (Some typ)); fixpoint_message None [name.v] diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 3402e05af8..58991f7156 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -19,7 +19,6 @@ open Constr open Declareops open Entries open Nameops -open Globnames open Pretyping open Termops open Reductionops @@ -117,10 +116,10 @@ let by tac pf = (* Support for mutually proved theorems *) let retrieve_first_recthm uctx = function - | VarRef id -> + | GlobRef.VarRef id -> NamedDecl.get_value (Global.lookup_named id), Decls.variable_opacity id - | ConstRef cst -> + | GlobRef.ConstRef cst -> let cb = Global.lookup_constant cst in (* we get the right order somehow but surely it could be enforced in a better way *) let uctx = UState.context uctx in @@ -178,12 +177,12 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recth in let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in let () = Declare.declare_variable ~name ~kind c in - (VarRef name,impargs) + (GlobRef.VarRef name,impargs) | Global local -> let kind = Decls.(IsAssumption Conjectural) in let decl = Declare.ParameterEntry (None,(t_i,univs),None) in let kn = Declare.declare_constant ~name ~local ~kind decl in - (ConstRef kn,impargs)) + (GlobRef.ConstRef kn,impargs)) | Some body -> let body = norm body in let rec body_i t = match Constr.kind t with @@ -201,11 +200,11 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recth let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in let c = Declare.SectionLocalDef const in let () = Declare.declare_variable ~name ~kind c in - (VarRef name,impargs) + (GlobRef.VarRef name,impargs) | Global local -> let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in - (ConstRef kn,impargs) + (GlobRef.ConstRef kn,impargs) let initialize_named_context_for_proof () = let sign = Global.named_context () in @@ -358,9 +357,9 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe in let kn = Declare.declare_constant ~name ~local ~kind:Decls.(IsAssumption Conjectural) (Declare.ParameterEntry pe) in let () = Declare.assumption_message name in - Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx); + Declare.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx); (* This takes care of the implicits and hook for the current constant*) - process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (ConstRef kn) impargs other_thms; + process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms; Feedback.feedback Feedback.AddedAxiom let save_lemma_admitted ~(lemma : t) : unit = @@ -418,14 +417,14 @@ let finish_proved env sigma idopt po info = let () = if should_suggest then Proof_using.suggest_variable (Global.env ()) name in - VarRef name + GlobRef.VarRef name | Global local -> let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in let () = if should_suggest then Proof_using.suggest_constant (Global.env ()) kn in - let gr = ConstRef kn in + let gr = GlobRef.ConstRef kn in Declare.declare_univ_binders gr (UState.universe_binders universes); gr in @@ -494,7 +493,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = in let entry, args = Abstract.shrink_entry local_context entry in let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in - let sigma, app = Evarutil.new_global sigma (ConstRef cst) in + let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in sigma, cst) sigma0 (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries diff --git a/vernac/record.ml b/vernac/record.ml index fe89303d33..86745212e7 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -14,7 +14,6 @@ open Term open Sorts open Util open Names -open Globnames open Nameops open Constr open Context @@ -362,10 +361,10 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f with Type_errors.TypeError (ctx,te) -> raise (NotDefinable (BadTypedProj (fid,ctx,te))) in - let refi = ConstRef kn in + let refi = GlobRef.ConstRef kn in Impargs.maybe_declare_manual_implicits false refi impls; if flags.pf_subclass then begin - let cl = Class.class_of_global (IndRef indsp) in + let cl = Class.class_of_global (GlobRef.IndRef indsp) in Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl end; let i = if is_local_assum decl then i+1 else i in @@ -468,7 +467,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let rsp = (kn, i) in (* This is ind path of idstruc *) let cstr = (rsp, 1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in - let build = ConstructRef cstr in + let build = GlobRef.ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false ~poly in let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in rsp @@ -514,9 +513,9 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari let proj_cst = Declare.declare_constant ~name:proj_name (DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition) in - let cref = ConstRef cst in + let cref = GlobRef.ConstRef cst in Impargs.declare_manual_implicits false cref paramimpls; - Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls); + Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls); Classes.set_typeclass_transparency (EvalConstRef cst) false false; let sub = match List.hd coers with | Some b -> Some ((if b then Backward else Forward), List.hd priorities) @@ -537,7 +536,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari let map ind = let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y) (List.rev fields) coers (Recordops.lookup_projections ind) - in IndRef ind, l + in GlobRef.IndRef ind, l in List.map map inds in @@ -580,14 +579,14 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari let add_constant_class env sigma cst = - let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in + let ty, univs = Typeops.type_of_global_in_context env (GlobRef.ConstRef cst) in let r = (Environ.lookup_constant cst env).const_relevance in let ctx, _ = decompose_prod_assum ty in let args = Context.Rel.to_extended_vect Constr.mkRel 0 ctx in let t = mkApp (mkConstU (cst, Univ.make_abstract_instance univs), args) in let tc = { cl_univs = univs; - cl_impl = ConstRef cst; + cl_impl = GlobRef.ConstRef cst; cl_context = (List.map (const None) ctx, ctx); cl_props = [LocalAssum (make_annot Anonymous r, t)]; cl_projs = []; @@ -609,7 +608,7 @@ let add_inductive_class env sigma ind = let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in let r = Inductive.relevance_of_inductive env ind in { cl_univs = univs; - cl_impl = IndRef ind; + cl_impl = GlobRef.IndRef ind; cl_context = List.map (const None) ctx, ctx; cl_props = [LocalAssum (make_annot Anonymous r, ty)]; cl_projs = []; @@ -628,8 +627,8 @@ let declare_existing_class g = if Typeclasses.is_class g then warn_already_existing_class g else match g with - | ConstRef x -> add_constant_class env sigma x - | IndRef x -> add_inductive_class env sigma x + | GlobRef.ConstRef x -> add_constant_class env sigma x + | GlobRef.IndRef x -> add_inductive_class env sigma x | _ -> user_err ~hdr:"declare_existing_class" (Pp.str"Unsupported class type, only constants and inductives are allowed") @@ -710,4 +709,4 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records = in let data = List.map2 map data records in let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in - List.map (fun ind -> IndRef ind) inds + List.map (fun ind -> GlobRef.IndRef ind) inds diff --git a/vernac/search.ml b/vernac/search.ml index 101a578587..dfb91d2d07 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -17,7 +17,6 @@ open Libobject open Environ open Pattern open Libnames -open Globnames module NamedDecl = Context.Named.Declaration @@ -53,7 +52,7 @@ module SearchBlacklist = let iter_constructors indsp u fn env nconstr = for i = 1 to nconstr do let typ = Inductiveops.type_of_constructor env ((indsp, i), u) in - fn (ConstructRef (indsp, i)) env typ + fn (GlobRef.ConstructRef (indsp, i)) env typ done let iter_named_context_name_type f = @@ -67,7 +66,7 @@ let get_current_or_goal_context ?pstate glnum = (* General search over hypothesis of a goal *) let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in - let iter_hyp idh typ = fn (VarRef idh) env typ in + let iter_hyp idh typ = fn (GlobRef.VarRef idh) env typ in let evmap,e = get_current_or_goal_context ?pstate glnum in let pfctxt = named_context e in iter_named_context_name_type iter_hyp pfctxt @@ -75,14 +74,14 @@ let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) = (* General search over declarations *) let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in - List.iter (fun d -> fn (VarRef (NamedDecl.get_id d)) env (NamedDecl.get_type d)) + List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) env (NamedDecl.get_type d)) (Environ.named_context env); let iter_obj (sp, kn) lobj = match lobj with | AtomicObject o -> begin match object_tag o with | "CONSTANT" -> let cst = Global.constant_of_delta_kn kn in - let gr = ConstRef cst in + let gr = GlobRef.ConstRef cst in let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in fn gr env typ | "INDUCTIVE" -> @@ -93,7 +92,7 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let i = (ind, u) in let typ = Inductiveops.type_of_inductive env i in - let () = fn (IndRef ind) env typ in + let () = fn (GlobRef.IndRef ind) env typ in let len = Array.length mip.mind_user_lc in iter_constructors ind u fn env len in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 255283ba36..68b7462bde 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -286,8 +286,8 @@ let print_strategy r = match r with | None -> let fold key lvl (vacc, cacc) = match key with - | VarKey id -> ((VarRef id, lvl) :: vacc, cacc) - | ConstKey cst -> (vacc, (ConstRef cst, lvl) :: cacc) + | VarKey id -> ((GlobRef.VarRef id, lvl) :: vacc, cacc) + | ConstKey cst -> (vacc, (GlobRef.ConstRef cst, lvl) :: cacc) | RelKey _ -> (vacc, cacc) in let var_lvl, cst_lvl = fold_strategy fold oracle ([], []) in @@ -304,7 +304,7 @@ let print_strategy r = var_msg ++ cst_msg | Some r -> let r = Smartlocate.smart_global r in - let key = match r with + let key = let open GlobRef in match r with | VarRef id -> VarKey id | ConstRef cst -> ConstKey cst | IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable") @@ -1459,7 +1459,7 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red if red_modifiers_specified then begin match sr with - | ConstRef _ as c -> + | GlobRef.ConstRef _ as c -> Reductionops.ReductionBehaviour.set ~local:section_local c (Option.get red_behavior) @@ -1731,8 +1731,8 @@ let vernac_set_strategy ~local l = let local = Option.default false local in let glob_ref r = match smart_global r with - | ConstRef sp -> EvalConstRef sp - | VarRef id -> EvalVarRef id + | GlobRef.ConstRef sp -> EvalConstRef sp + | GlobRef.VarRef id -> EvalVarRef id | _ -> user_err Pp.(str "cannot set an inductive type or a constructor as transparent") in let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in @@ -1742,8 +1742,8 @@ let vernac_set_opacity ~local (v,l) = let local = Option.default true local in let glob_ref r = match smart_global r with - | ConstRef sp -> EvalConstRef sp - | VarRef id -> EvalVarRef id + | GlobRef.ConstRef sp -> EvalConstRef sp + | GlobRef.VarRef id -> EvalVarRef id | _ -> user_err Pp.(str "cannot set an inductive type or a constructor as transparent") in let l = List.map glob_ref l in @@ -2090,7 +2090,7 @@ let vernac_register qid r = match r with | RegisterInline -> begin match gr with - | ConstRef c -> Global.register_inline c + | GlobRef.ConstRef c -> Global.register_inline c | _ -> CErrors.user_err (Pp.str "Register Inline: expecting a constant") end | RegisterCoqlib n -> @@ -2106,7 +2106,7 @@ let vernac_register qid r = | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace") in match gr with - | IndRef ind -> Global.register_inductive ind pind + | GlobRef.IndRef ind -> Global.register_inductive ind pind | _ -> CErrors.user_err (Pp.str "Register in kernel: expecting an inductive type") end else Coqlib.register_ref (Libnames.string_of_qualid n) gr |