diff options
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 30dd6ec74..ce74f2344 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 @@ -334,8 +334,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 +436,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 +451,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 |