aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml12
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/lemmas.ml20
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernacentries.ml8
6 files changed, 22 insertions, 28 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 59920742d..503508fc0 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -533,7 +533,7 @@ open Namegen
let compute_bl_goal ind lnamesparrec nparrec =
let eqI, eff = eqI ind lnamesparrec in
let list_id = list_id lnamesparrec in
- let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
let create_input c =
let x = next_ident_away (Id.of_string "x") avoid and
y = next_ident_away (Id.of_string "y") avoid in
@@ -578,7 +578,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
in
let fresh_id s gl =
- let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
+ let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
in
Proofview.Goal.enter begin fun gl ->
@@ -676,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
let compute_lb_goal ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
- let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
let eqI, eff = eqI ind lnamesparrec in
let create_input c =
let x = next_ident_away (Id.of_string "x") avoid and
@@ -722,7 +722,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
( List.map (fun (_,_,_,slb) -> slb) list_id )
in
let fresh_id s gl =
- let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
+ let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
in
Proofview.Goal.enter begin fun gl ->
@@ -806,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec =
check_not_is_defined ();
let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
let list_id = list_id lnamesparrec in
- let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
+ let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
let create_input c =
let x = next_ident_away (Id.of_string "x") avoid and
y = next_ident_away (Id.of_string "y") avoid in
@@ -870,7 +870,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
( List.map (fun (_,_,_,slb) -> slb) list_id )
in
let fresh_id s gl =
- let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
+ let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
in
Proofview.Goal.enter begin fun gl ->
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c21345a2a..0926c93e5 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -183,7 +183,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
id
| Anonymous ->
let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
- Namegen.next_global_ident_away i (Termops.ids_of_context env)
+ Namegen.next_global_ident_away i (Termops.vars_of_env env)
in
let env' = push_rel_context ctx env in
evars := Evarutil.nf_evar_map !evars;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 4b36c2d07..2c8f6ec9d 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -211,7 +211,8 @@ let compute_proof_name locality = function
user_err ?loc (pr_id id ++ str " already exists.");
id
| None ->
- next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ())
+ let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
+ next_global_ident_away default_thm_id avoid
let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) =
let t_i = norm t_i in
@@ -309,12 +310,6 @@ let get_proof proof do_guard hook opacity =
in
id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
-let check_exist =
- List.iter (fun (loc,id) ->
- if not (Nametab.exists_cci (Lib.make_path id)) then
- user_err ?loc (pr_id id ++ str " does not exist.")
- )
-
let universe_proof_terminator compute_guard hook =
let open Proof_global in
make_terminator begin function
@@ -322,17 +317,16 @@ let universe_proof_terminator compute_guard hook =
admit (id,k,pe) pl (hook (Some ctx)) ();
Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
- let is_opaque, export_seff, exports = match opaque with
- | Vernacexpr.Transparent -> false, true, []
- | Vernacexpr.Opaque None -> true, false, []
- | Vernacexpr.Opaque (Some l) -> true, true, l in
+ let is_opaque, export_seff = match opaque with
+ | Vernacexpr.Transparent -> false, true
+ | Vernacexpr.Opaque -> true, false
+ in
let proof = get_proof proof compute_guard
(hook (Some (fst proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
| Some (_,id) -> save_anonymous ~export_seff proof id
- end;
- check_exist exports
+ end
end
let standard_proof_terminator compute_guard hook =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 89b18d254..81218308f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -846,9 +846,9 @@ let obligation_terminator name num guard hook auto pf =
let obl = obls.(num) in
let status =
match obl.obl_status, opq with
- | (_, Evar_kinds.Expand), Vernacexpr.Opaque _ -> err_not_transp ()
- | (true, _), Vernacexpr.Opaque _ -> err_not_transp ()
- | (false, _), Vernacexpr.Opaque _ -> Evar_kinds.Define true
+ | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
+ | (true, _), Vernacexpr.Opaque -> err_not_transp ()
+ | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
| (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false
| (_, status), Vernacexpr.Transparent -> status
in
diff --git a/vernac/record.ml b/vernac/record.ml
index 4fb607dec..18e7796ca 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -457,7 +457,7 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
let impls = implicits_of_context params in
List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
in
- let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
+ let binder_name = Namegen.next_ident_away (snd id) (Termops.vars_of_env (Global.env())) in
let impl, projs =
match fields with
| [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ee84ff101..83296cf58 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -125,8 +125,8 @@ let make_cases_aux glob_ref =
| [] -> []
| (n,_)::l ->
let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
- Id.to_string n' :: rename (n'::avoid) l in
- let al' = rename [] al 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
(Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
tarr []
@@ -507,7 +507,7 @@ let vernac_exact_proof c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the begining of a proof. *)
let status = Pfedit.by (Tactics.exact_proof c) in
- save_proof (Vernacexpr.(Proved(Opaque None,None)));
+ save_proof (Vernacexpr.(Proved(Opaque,None)));
if not status then Feedback.feedback Feedback.AddedAxiom
let vernac_assumption locality poly (local, kind) l nl =
@@ -1230,7 +1230,7 @@ let vernac_reserve bl =
let env = Global.env() in
let sigma = Evd.from_env env in
let t,ctx = Constrintern.interp_type env sigma c in
- let t = Detyping.detype Detyping.Now false [] env (Evd.from_ctx ctx) (EConstr.of_constr t) in
+ let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) (EConstr.of_constr t) in
let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
Reserve.declare_reserved_type idl t)
in List.iter sb_decl bl
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 15:40:55 +0000