diff options
Diffstat (limited to 'plugins')
50 files changed, 266 insertions, 309 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index e34150f2b3..ead78f70a1 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -20,7 +20,7 @@ let start_deriving f suchthat name : Lemmas.t = let env = Global.env () in let sigma = Evd.from_env env in let poly = false in - let kind = Decl_kinds.(DefinitionBody Definition) in + let kind = Decls.(IsDefinition Definition) in (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 9abf212443..1c325a8d3a 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 @@ -125,7 +124,7 @@ module KOrd = struct type t = kind * string let compare (k1, s1) (k2, s2) = - let c = Pervasives.compare k1 k2 (* OK *) in + let c = pervasives_compare k1 k2 (* OK *) in if c = 0 then String.compare s1 s2 else c end @@ -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 7ee8d7f342..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 @@ -29,24 +28,27 @@ open Common let toplevel_env () = let get_reference = function - | (_,kn), Lib.Leaf o -> - let mp,l = KerName.repr kn in - begin match Libobject.object_tag o with - | "CONSTANT" -> - let constant = Global.lookup_constant (Constant.make1 kn) in - Some (l, SFBconst constant) - | "INDUCTIVE" -> - let inductive = Global.lookup_mind (MutInd.make1 kn) in - Some (l, SFBmind inductive) - | "MODULE" -> - let modl = Global.lookup_module (MPdot (mp, l)) in - Some (l, SFBmodule modl) - | "MODULE TYPE" -> - let modtype = Global.lookup_modtype (MPdot (mp, l)) in - Some (l, SFBmodtype modtype) - | "INCLUDE" -> user_err Pp.(str "No extraction of toplevel Include yet.") - | _ -> None - end + | (_,kn), Lib.Leaf Libobject.AtomicObject o -> + let mp,l = KerName.repr kn in + begin match Libobject.object_tag o with + | "CONSTANT" -> + let constant = Global.lookup_constant (Constant.make1 kn) in + Some (l, SFBconst constant) + | "INDUCTIVE" -> + let inductive = Global.lookup_mind (MutInd.make1 kn) in + Some (l, SFBmind inductive) + | _ -> None + end + | (_,kn), Lib.Leaf Libobject.ModuleObject _ -> + let mp,l = KerName.repr kn in + let modl = Global.lookup_module (MPdot (mp, l)) in + Some (l, SFBmodule modl) + | (_,kn), Lib.Leaf Libobject.ModuleTypeObject _ -> + let mp,l = KerName.repr kn in + let modtype = Global.lookup_modtype (MPdot (mp, l)) in + Some (l, SFBmodtype modtype) + | (_,kn), Lib.Leaf Libobject.IncludeObject _ -> + user_err Pp.(str "No extraction of toplevel Include yet.") | _ -> None in List.rev (List.map_filter get_reference (Lib.contents ())) @@ -115,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 @@ -758,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 f773b2c39e..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 @@ -79,7 +78,7 @@ let do_observe_tac s tac g = with reraise -> let reraise = CErrors.push reraise in if not (Stack.is_empty debug_queue) - then print_debug_queue (Some (fst (ExplainErr.process_vernac_interp_error reraise))); + then print_debug_queue (Some (fst reraise)); iraise reraise let observe_tac_stream s tac g = @@ -992,7 +991,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in + ~kind:(Decls.(IsProof Theorem)) () in let lemma = Lemmas.start_lemma (*i The next call to mk_equation_id is valid since we are constructing the lemma @@ -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 3bab750534..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 @@ -369,9 +369,9 @@ let generate_functional_principle (evd: Evd.evar_map ref) let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant - name - (Declare.DefinitionEntry ce, - Decl_kinds.IsDefinition (Decl_kinds.Scheme)) + ~name + ~kind:Decls.(IsDefinition Scheme) + (Declare.DefinitionEntry ce) ); Declare.definition_message name; names := name :: !names @@ -387,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in - save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem) + save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decls.(IsProof Theorem) with e when CErrors.noncritical e -> raise (Defining_principle e) @@ -637,8 +637,9 @@ let build_scheme fas = (fun (princ_id,_,_) def_entry -> ignore (Declare.declare_constant - princ_id - (Declare.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + ~name:princ_id + ~kind:Decls.(IsProof Theorem) + (Declare.DefinitionEntry def_entry)); Declare.definition_message princ_id ) fas diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index e20d010c71..5f859b3e4b 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -227,7 +227,6 @@ END { let warning_error names e = - let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> let names = pr_enum Libnames.pr_qualid names in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index bb4e745fe9..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) @@ -1506,7 +1505,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false ~poly:false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds ~cumulative:false ~poly:false ~private_ind:false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> 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 d305a58ccc..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, @@ -244,9 +243,6 @@ let prepare_body ((name,_,args,types,_),_) rt = let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') -let process_vernac_interp_error e = - fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)) - let warn_funind_cannot_build_inversion = CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind" (fun e' -> strbrk "Cannot build inversion information" ++ @@ -293,11 +289,9 @@ let derive_inversion fix_names = fix_names_as_constant lind; with e when CErrors.noncritical e -> - let e' = process_vernac_interp_error e in - warn_funind_cannot_build_inversion e' + warn_funind_cannot_build_inversion e with e when CErrors.noncritical e -> - let e' = process_vernac_interp_error e in - warn_funind_cannot_build_inversion e' + warn_funind_cannot_build_inversion e let warn_cannot_define_graph = CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind" @@ -310,17 +304,13 @@ let warn_cannot_define_principle = h 1 names ++ error) let warning_error names e = - let e = process_vernac_interp_error e in let e_explain e = match e with | ToShow e -> - let e = process_vernac_interp_error e in spc () ++ CErrors.print e | _ -> if do_observe () - then - let e = process_vernac_interp_error e in - (spc () ++ CErrors.print e) + then (spc () ++ CErrors.print e) else mt () in match e with @@ -333,7 +323,6 @@ let warning_error names e = | _ -> raise e let error_error names e = - let e = process_vernac_interp_error e in let e_explain e = match e with | ToShow e -> spc () ++ CErrors.print e @@ -419,7 +408,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ~name:fname ~poly:false ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decl_kinds.Definition pl + ~kind:Decls.Definition pl bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left @@ -846,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 56ed406e2f..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 @@ -123,21 +122,19 @@ open DeclareDef let definition_message = Declare.definition_message -let save id const ?hook uctx scope kind = +let save name const ?hook uctx scope kind = let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in let r = match scope with | Discharge -> - let k = Kindops.logical_kind_of_goal_kind kind in - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - VarRef id + let c = SectionLocalDef const in + let () = declare_variable ~name ~kind c in + GlobRef.VarRef name | Global local -> - let k = Kindops.logical_kind_of_goal_kind kind in - let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in - ConstRef kn + let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in + GlobRef.ConstRef kn in DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r }); - definition_message id + definition_message name let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () @@ -277,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 () ++ @@ -301,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 @@ -330,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; @@ -435,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/indfun_common.mli b/plugins/funind/indfun_common.mli index 45d332031f..a95b1242ac 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -48,7 +48,7 @@ val save -> ?hook:DeclareDef.Hook.t -> UState.t -> DeclareDef.locality - -> Decl_kinds.goal_object_kind + -> Decls.logical_kind -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 86defb2f2f..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 @@ -54,9 +53,8 @@ let do_observe_tac s tac g = msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v with reraise -> let reraise = CErrors.push reraise in - let e = ExplainErr.process_vernac_interp_error reraise in observe (hov 0 (str "observation "++ s++str " raised exception " ++ - CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal )); + CErrors.iprint reraise ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; let observe_tac s tac g = @@ -94,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 @@ -166,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 @@ -805,7 +803,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let (typ,_) = lemmas_types_infos.(i) in let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in + ~kind:(Decls.(IsProof Theorem)) () in let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false @@ -871,7 +869,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let lem_id = mk_complete_id f_id in let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decl_kinds.(Proof Theorem) () in + ~kind:Decls.(IsProof Theorem) () in let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by @@ -979,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 d38e28c0e7..937118bf57 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -30,7 +30,6 @@ open Tacmach open Tactics open Nametab open Declare -open Decl_kinds open Tacred open Goal open Glob_term @@ -66,9 +65,9 @@ let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in locate (make_qualid dp (Id.of_string s)) -let declare_fun f_id kind ?univs value = +let declare_fun name kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in - ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; + GlobRef.ConstRef(declare_constant ~name ~kind (DefinitionEntry ce)) let defined lemma = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None @@ -96,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 *) @@ -196,7 +195,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) = let body = EConstr.Unsafe.to_constr body in it_mkLambda_or_LetIn body context -let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) = +let (declare_f : Id.t -> Decls.logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -211,7 +210,7 @@ let print_debug_queue b e = begin let lmsg,goal = Stack.pop debug_queue in if b then - Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal)) + Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.iprint e) ++ str " on goal" ++ fnl() ++ goal)) else begin Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); @@ -238,7 +237,7 @@ let do_observe_tac s tac g = with reraise -> let reraise = CErrors.push reraise in if not (Stack.is_empty debug_queue) - then print_debug_queue true (fst (ExplainErr.process_vernac_interp_error reraise)); + then print_debug_queue true reraise; iraise reraise let observe_tac s tac g = @@ -1313,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 @@ -1368,7 +1367,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None in let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma) + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decls.(IsProof Lemma)) () in let lemma = Lemmas.start_lemma ~name:na @@ -1411,10 +1410,9 @@ let com_terminate nb_args ctx hook = let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = - let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in + let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(IsProof Lemma) () in let lemma = Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) - ~sign:(Environ.named_context_val env) ~info ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) in @@ -1452,17 +1450,17 @@ let start_equation (f:GlobRef.t) (term_f:GlobRef.t) Array.of_list (List.map mkVar x))))); observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x)]) g;; -let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type = +let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type = 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 let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~sign evd + let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false evd (EConstr.of_constr equation_lemma_type) in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (start_equation f_ref terminate_ref @@ -1535,7 +1533,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type let term_id = add_suffix function_name "_terminate" in let functional_ref = let univs = Evd.univ_entry ~poly:false evd in - declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res + declare_fun functional_id Decls.(IsDefinition Definition) ~univs res in (* Refresh the global universes, now including those of _F *) let evd = Evd.from_env (Global.env ()) in @@ -1549,14 +1547,13 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) let hook { DeclareDef.Hook.S.uctx ; _ } = let term_ref = Nametab.locate (qualid_of_ident term_id) in - let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in + let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref in let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in (* message "start second proof"; *) let stop = (* XXX: What is the correct way to get sign at hook time *) - let sign = Environ.named_context_val Global.(env ()) in try - com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); + com_eqn uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); false with e when CErrors.noncritical e -> begin 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/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 243e0e945c..9d46bbc74e 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -376,7 +376,7 @@ let get_local_profiling_results () = List.hd Local.(!stack) own. *) module DData = struct type t = Feedback.doc_id * Stateid.t - let compare x y = Pervasives.compare x y + let compare x y = compare x y end module SM = Map.Make(DData) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 19866df8e3..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 @@ -1898,11 +1897,11 @@ let declare_projection n instance_id r = let univs = Evd.univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in - let cst = - Declare.definition_entry ~types:typ ~univs term - in - ignore(Declare.declare_constant n - (Declare.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) + let cst = Declare.definition_entry ~types:typ ~univs term in + let _ : Constant.t = + Declare.declare_constant ~name:n ~kind:Decls.(IsDefinition Definition) + (Declare.DefinitionEntry cst) + in () let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in @@ -1978,14 +1977,13 @@ let add_morphism_as_parameter atts m n : unit = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in - let cst = Declare.declare_constant instance_id - (Declare.ParameterEntry - (None,(instance,uctx),None), - Decl_kinds.IsAssumption Decl_kinds.Logical) + let cst = Declare.declare_constant ~name:instance_id + ~kind:Decls.(IsAssumption Logical) + (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 (); @@ -1995,14 +1993,14 @@ let add_morphism_interactive atts m n : Lemmas.t = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in let poly = atts.polymorphic in - let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in + 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/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 3014ba5115..539536911c 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -33,12 +33,8 @@ type debug_info = | DebugOff (* An exception handler *) -let explain_logic_error e = - CErrors.print (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null))) - -let explain_logic_error_no_anomaly e = - CErrors.print_no_report - (fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null))) +let explain_logic_error e = CErrors.print e +let explain_logic_error_no_anomaly e = CErrors.print_no_report e let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl()) let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) @@ -160,7 +156,7 @@ let rec prompt level = begin let open Proofview.NonLogical in Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> - if Pervasives.(!batch) then return (DebugOn (level+1)) else + if Util.(!batch) then return (DebugOn (level+1)) else let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with @@ -370,8 +366,9 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - (* XXX: This hooks into the ExplainErr extension API - so it is tricky to provide the right env for now. *) + (* XXX: This hooks into the CErrors's additional error + info API so it is tricky to provide the right env for + now. *) let env = Global.env () in let sigma = Evd.from_env env in Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) @@ -424,11 +421,11 @@ let extract_ltac_trace ?loc trace = aux loc trace in best_loc, None -let get_ltac_trace (_, info) = +let get_ltac_trace info = let ltac_trace = Exninfo.get info ltac_trace_info in let loc = Loc.get_loc info in match ltac_trace with | None -> None | Some trace -> Some (extract_ltac_trace ?loc trace) -let () = ExplainErr.register_additional_error_info get_ltac_trace +let () = CErrors.register_additional_error_info get_ltac_trace diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 2e32b00c25..24039c93c6 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -93,7 +93,7 @@ let dev_form n_spec p = let rec fixpoint f x = let y' = f x in - if Pervasives.(=) y' x then y' + if (=) y' x then y' else fixpoint f y' let rec_simpl_cone n_spec e = diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index f0435126aa..5cc2c2e061 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1585,7 +1585,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) = let hyps_idx = prover.hyps prf in let hyps = selecti hyps_idx old_cl in - is_sublist Pervasives.(=) hyps new_cl in + is_sublist (=) hyps new_cl in @@ -1953,7 +1953,7 @@ open Persistent_cache module Cache = PHashtable(struct type t = (provername * micromega_polys) - let equal = Pervasives.(=) + let equal = (=) let hash = Hashtbl.hash end) diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml index d8f71cda0c..cf5f60fb55 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -136,7 +136,7 @@ let pure_sos l = I should nonetheless be able to try something - over Z > is equivalent to -1 >= *) try let l = List.combine l (CList.interval 0 (List.length l -1)) in - let (lt,i) = try (List.find (fun (x,_) -> Pervasives.(=) (snd x) Mc.Strict) l) + let (lt,i) = try (List.find (fun (x,_) -> (=) (snd x) Mc.Strict) l) with Not_found -> List.hd l in let plt = poly_neg (poly_of_term (expr_to_term (fst lt))) in let (n,polys) = sumofsquares plt in (* n * (ci * pi^2) *) diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 34fb32c270..943bcb384b 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -15,7 +15,7 @@ open Vect let debug = false -let compare_float (p : float) q = Pervasives.compare p q +let compare_float (p : float) q = pervasives_compare p q (** Implementation of intervals *) open Itv @@ -587,7 +587,7 @@ struct let optimise vect l = (* We add a dummy (fresh) variable for vector *) let fresh = - List.fold_left (fun fr c -> Pervasives.max fr (Vect.fresh c.coeffs)) 0 l in + List.fold_left (fun fr c -> max fr (Vect.fresh c.coeffs)) 0 l in let cstr = { coeffs = Vect.set fresh (Int (-1)) vect ; op = Eq ; diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 97cf23ac1f..537b6175b4 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -21,7 +21,7 @@ module Int = struct type t = int - let compare : int -> int -> int = Pervasives.compare + let compare : int -> int -> int = compare let equal : int -> int -> bool = (=) end @@ -354,7 +354,7 @@ struct let from i = i let next i = i + 1 - let max : int -> int -> int = Pervasives.max + let max : int -> int -> int = max let pp o i = output_string o (string_of_int i) let compare : int -> int -> int = Int.compare let to_int x = x diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index f909b4ecda..1a31a36732 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -278,7 +278,7 @@ and op = |Eq | Ge | Gt exception Strict -let is_strict c = Pervasives.(=) c.op Gt +let is_strict c = (=) c.op Gt let eval_op = function | Eq -> (=/) @@ -422,7 +422,7 @@ module LinPoly = struct let min_list (l:int list) = match l with | [] -> None - | e::l -> Some (List.fold_left Pervasives.min e l) + | e::l -> Some (List.fold_left min e l) let search_linear p l = min_list (search_all_linear p l) @@ -656,9 +656,9 @@ module ProofFormat = struct let rec compare p1 p2 = match p1, p2 with | Annot(s1,p1) , Annot(s2,p2) -> if s1 = s2 then compare p1 p2 - else Pervasives.compare s1 s2 - | Hyp i , Hyp j -> Pervasives.compare i j - | Def i , Def j -> Pervasives.compare i j + else Util.pervasives_compare s1 s2 + | Hyp i , Hyp j -> Util.pervasives_compare i j + | Def i , Def j -> Util.pervasives_compare i j | Cst n , Cst m -> Num.compare_num n m | Zero , Zero -> 0 | Square v1 , Square v2 -> Vect.compare v1 v2 @@ -667,7 +667,7 @@ module ProofFormat = struct | MulPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2) | AddPrf(p1,q1) , MulPrf(p2,q2) -> cmp_pair compare compare (p1,q1) (p2,q2) | CutPrf p , CutPrf p' -> compare p p' - | _ , _ -> Pervasives.compare (id_of_constr p1) (id_of_constr p2) + | _ , _ -> Util.pervasives_compare (id_of_constr p1) (id_of_constr p2) end @@ -785,7 +785,7 @@ module ProofFormat = struct let rec xid_of_hyp i l' = match l' with | [] -> failwith (Printf.sprintf "id_of_hyp %i %s" hyp (string_of_int_list l)) - | hyp'::l' -> if Pervasives.(=) hyp hyp' then i else xid_of_hyp (i+1) l' in + | hyp'::l' -> if (=) hyp hyp' then i else xid_of_hyp (i+1) l' in xid_of_hyp 0 l end @@ -873,7 +873,7 @@ module ProofFormat = struct let (p,o) = eval_prf_rule (fun i -> IMap.find i env) prf in if is_unsat (p,o) then true else - if Pervasives.(=) rst Done + if (=) rst Done then begin Printf.fprintf stdout "Last inference %a %s\n" LinPoly.pp p (string_of_op o); diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index 15fb55c007..4c95e6da75 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -587,7 +587,7 @@ let cut env rmin sol vm (rst:Restricted.t) tbl (x,v) = Printf.printf "This is a cutting plane for %a:" LinPoly.pp_var x; Printf.printf " %a\n" WithProof.output (v,prf); end; - if Pervasives.(=) (snd v) Eq + if (=) (snd v) Eq then (* Unsat *) Some (x,(v,prf)) else let vl = (Vect.dotproduct (fst v) (Vect.set 0 (Int 1) sol)) in @@ -651,7 +651,7 @@ let integer_solver lp = match find_cut (!nb mod 2) env cr (*x*) sol vm rst tbl with | None -> None | Some(cr,((v,op),cut)) -> - if Pervasives.(=) op Eq + if (=) op Eq then (* This is a contradiction *) Some(Step(vr,CutPrf cut, Done)) else diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index e3a9f6f60f..58d5d7ecf1 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -13,7 +13,7 @@ open Num (* Comparisons that are reflexive on NaN and also short-circuiting. *) (* ------------------------------------------------------------------------- *) -let cmp = Pervasives.compare (** FIXME *) +let cmp = compare (** FIXME *) let (=?) = fun x y -> cmp x y = 0;; let (<?) = fun x y -> cmp x y < 0;; @@ -491,21 +491,21 @@ let temp_path = Filename.get_temp_dir_name ();; (* ------------------------------------------------------------------------- *) let strings_of_file filename = - let fd = try Pervasives.open_in filename + let fd = try open_in filename with Sys_error _ -> failwith("strings_of_file: can't open "^filename) in let rec suck_lines acc = - try let l = Pervasives.input_line fd in + try let l = input_line fd in suck_lines (l::acc) with End_of_file -> List.rev acc in let data = suck_lines [] in - (Pervasives.close_in fd; data);; + (close_in fd; data);; let string_of_file filename = String.concat "\n" (strings_of_file filename);; let file_of_string filename s = - let fd = Pervasives.open_out filename in + let fd = open_out filename in output_string fd s; close_out fd;; diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index 4b2bc66eb7..a5f3b83c48 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -148,7 +148,7 @@ let rec add (ve1:t) (ve2:t) = match ve1 , ve2 with | [] , v | v , [] -> v | (v1,c1)::l1 , (v2,c2)::l2 -> - let cmp = Pervasives.compare v1 v2 in + let cmp = Util.pervasives_compare v1 v2 in if cmp == 0 then let s = add_num c1 c2 in if eq_num (Int 0) s @@ -163,7 +163,7 @@ let rec xmul_add (n1:num) (ve1:t) (n2:num) (ve2:t) = | [] , _ -> mul n2 ve2 | _ , [] -> mul n1 ve1 | (v1,c1)::l1 , (v2,c2)::l2 -> - let cmp = Pervasives.compare v1 v2 in + let cmp = Util.pervasives_compare v1 v2 in if cmp == 0 then let s = ( n1 */ c1) +/ (n2 */ c2) in if eq_num (Int 0) s diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 6aec83318c..00ea9b6a66 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") @@ -500,7 +499,7 @@ let context sigma operation path (t : constr) = | (p, Fix ((_,n as ln),(tys,lna,v))) -> let l = Array.length v in let v' = Array.copy v in - v'.(n)<- loop (Pervasives.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) + v'.(n)<- loop (Util.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v'))) | ((P_TYPE :: p), Prod (n,t,c)) -> (mkProd (n,loop i p t,c)) | ((P_TYPE :: p), Lambda (n,t,c)) -> @@ -684,7 +683,7 @@ let simpl_coeffs path_init path_k = | _ -> assert false) | _ -> assert false in - let n = Pervasives.(-) (List.length path_k) (List.length path_init) in + let n = Util.(-) (List.length path_k) (List.length path_init) in let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) in convert_concl ~check:false newc DEFAULTcast @@ -1000,7 +999,7 @@ let shrink_pair p f1 f2 = | t1,t2 -> begin oprint t1; print_newline (); oprint t2; print_newline (); - flush Pervasives.stdout; CErrors.user_err Pp.(str "shrink.1") + flush stdout; CErrors.user_err Pp.(str "shrink.1") end let reduce_factor p = function diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index cec87221f0..05c31062fc 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -242,7 +242,7 @@ let add_event, history, clear_history = (fun () -> !accu), (fun () -> accu := []) -let nf_linear = List.sort (fun x y -> Pervasives.(-) y.v x.v) +let nf_linear = List.sort (fun x y -> Util.(-) y.v x.v) let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x)) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 33798c43c8..eb75fca0a1 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -29,7 +29,6 @@ open Tacinterp open Libobject open Printer open Declare -open Decl_kinds open Entries open Newring_ast open Proofview.Notations @@ -50,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 @@ -156,9 +155,9 @@ let decl_constant na univs c = let () = Declare.declare_universe_context ~poly:false univs in let types = (Typeops.infer (Global.env ()) c).uj_type in let univs = Monomorphic_entry Univ.ContextSet.empty in - mkConst(declare_constant (Id.of_string na) - (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c), - IsProof Lemma)) + mkConst(declare_constant ~name:(Id.of_string na) + ~kind:Decls.(IsProof Lemma) + (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c))) (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = 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/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 279e7ce1a6..0adabb0673 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -412,11 +412,10 @@ let interp_search_arg arg = if is_ident_part s then Search.GlobSearchString s else interp_search_notation ~loc s key | RGlobSearchSubPattern p -> - try - let env = Global.env () in - let _, p = Constrintern.intern_constr_pattern env (Evd.from_env env) p in - Search.GlobSearchSubPattern p - with e -> let e = CErrors.push e in iraise (ExplainErr.process_vernac_interp_error e)) arg in + let env = Global.env () in + let _, p = Constrintern.intern_constr_pattern env (Evd.from_env env) p in + Search.GlobSearchSubPattern p) arg + in let hpat, a1 = match arg with | (_, Search.GlobSearchSubPattern (Pattern.PMeta _)) :: a' -> all_true, a' | (true, Search.GlobSearchSubPattern p) :: a' -> diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 34f13b1096..f91b5e7aa2 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -26,7 +26,7 @@ module AdaptorDb = struct module AdaptorKind = struct type t = kind - let compare = Pervasives.compare + let compare = pervasives_compare end module AdaptorMap = Map.Make(AdaptorKind) 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 |