diff options
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 30 |
1 files changed, 13 insertions, 17 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 30dd6ec7..880a11be 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -34,7 +34,7 @@ open Impargs module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a +type 'a declaration_hook = Decl_kinds.locality -> GlobRef.t -> 'a let mk_hook hook = hook let call_hook fix_exn hook l c = try hook l c @@ -71,17 +71,13 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) - let add c cb e = - let exists c e = - try ignore(Environ.lookup_constant c e); true - with Not_found -> false in - if exists c e then e else Environ.add_constant c cb e in - let env = List.fold_left (fun env { eff } -> - match eff with - | SEsubproof (c, cb,_) -> add c cb env - | SEscheme (l,_) -> - List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) - env (Safe_typing.side_effects_of_private_constants eff) in + let fold env eff = + try + let _ = Environ.lookup_constant eff.seff_constant env in + env + with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env + in + let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in let indexes = search_guard env possible_indexes fixdecls in @@ -334,8 +330,8 @@ let universe_proof_terminator compute_guard hook = Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff = match opaque with - | Vernacexpr.Transparent -> false, true - | Vernacexpr.Opaque -> true, false + | Transparent -> false, true + | Opaque -> true, false in let proof = get_proof proof compute_guard (hook (Some (proof.Proof_global.universes))) is_opaque in @@ -436,7 +432,7 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook = let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in let decl = fst (List.hd thms) in - let evd, decl = Univdecls.interp_univ_decl_opt env0 (snd decl) in + let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in @@ -451,12 +447,12 @@ let start_proof_com ?inference_hook kind thms hook = (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) evd thms in let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in - let evd, _nf = Evarutil.nf_evars_and_universes evd in + let evd = Evd.minimize_universes evd in (* XXX: This nf_evar is critical too!! We are normalizing twice if you look at the previous lines... *) let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in let () = - let open Misctypes in + let open UState in if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl) in |