diff options
31 files changed, 225 insertions, 242 deletions
diff --git a/library/universes.ml b/library/universes.ml index be49294a2..e2a3901ba 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -791,18 +791,17 @@ let normalize_context_set ctx us algs = in let partition = UF.partition uf in let flex x = LMap.mem x us in - let subst, eqs = List.fold_left (fun (subst, cstrs) s -> + let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in (* Add equalities for globals which can't be merged anymore. *) let cstrs = LSet.fold (fun g cst -> - Constraint.add (canon, Univ.Eq, g) cst) (LSet.union global rigid) + Constraint.add (canon, Univ.Eq, g) cst) global cstrs in - let subst = LSet.fold (fun f -> LMap.add f canon) - flexible subst - in - (subst, cstrs)) - (LMap.empty, Constraint.empty) partition + let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in + let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in + (LSet.diff (LSet.diff ctx rigid) flexible, subst, cstrs)) + (ctx, LMap.empty, Constraint.empty) partition in (* Noneqs is now in canonical form w.r.t. equality constraints, and contains only inequality constraints. *) diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml index 160e905f8..1601a7ce2 100644 --- a/plugins/Derive/derive.ml +++ b/plugins/Derive/derive.ml @@ -15,7 +15,7 @@ let interp_init_def_and_relation env sigma init_def r = mkProd (Names.Anonymous,init_type, mkProd (Names.Anonymous,init_type,mkProp)) in let r, ctx = Constrintern.interp_casted_constr sigma env r r_type in - init_def , init_type , r, Evd.evar_universe_context_set ctx + init_def , init_type , r, ctx (** [start_deriving f init r lemma] starts a proof of [r init @@ -23,14 +23,15 @@ let interp_init_def_and_relation env sigma init_def r = [lemma] as the proof. *) let start_deriving f init_def r lemma = let env = Global.env () in + let sigma = Evd.from_env env in let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in let ( init_def , init_type , r , ctx ) = - interp_init_def_and_relation env Evd.empty init_def r + interp_init_def_and_relation env sigma init_def r in let goals = let open Proofview in - TCons ( env , (init_type , ctx ) , (fun ef -> - TCons ( env , ( Term.mkApp ( r , [| init_def ; ef |] ) , Univ.ContextSet.empty) , (fun _ -> TNil)))) + TCons ( env , (init_type ) , (fun ef -> + TCons ( env , ( Term.mkApp ( r , [| init_def ; ef |] )) , (fun _ -> TNil)))) in let terminator com = let open Proof_global in @@ -65,7 +66,7 @@ let start_deriving f init_def r lemma = ignore (Declare.declare_constant lemma lemma_def) in let () = Proof_global.start_dependent_proof - lemma kind goals terminator + lemma kind ctx goals terminator in let _ = Proof_global.with_current_proof begin fun _ p -> Proof.run_tactic env Proofview.(tclFOCUS 1 1 shelve) p diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 9589e51f4..841796ed7 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -987,8 +987,9 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = i*) (mk_equation_id f_id) (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) - (lemma_type, (*FIXME*) Univ.ContextSet.empty) - (Lemmas.mk_hook (fun _ _ -> ())); + Evd.empty_evar_universe_context + lemma_type + (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); Lemmas.save_proof (Vernacexpr.Proved(false,None)) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 8c3033d0c..c4a340880 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -278,7 +278,8 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro Lemmas.start_proof new_princ_name (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) - (new_principle_type, (*FIXME*) Univ.ContextSet.empty) + (*FIXME*) Evd.empty_evar_universe_context + new_principle_type hook ; (* let _tim1 = System.get_time () in *) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 20304b529..52d3b4a87 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1079,7 +1079,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g let lem_id = mk_correct_id f_id in Lemmas.start_proof lem_id (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) - (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty) + (*FIXME*) Evd.empty_evar_universe_context + (fst lemmas_types_infos.(i)) (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") @@ -1132,7 +1133,8 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) - (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty) + (*FIXME*) Evd.empty_evar_universe_context + (fst lemmas_types_infos.(i)) (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 961266c9c..f141d3619 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1269,7 +1269,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos let lid = ref [] in let h_num = ref (-1) in Proof_global.discard_all (); - build_proof (Univ.ContextSet.empty) + build_proof Evd.empty_evar_universe_context ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in tclTHENSEQ @@ -1317,7 +1317,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos Lemmas.start_proof na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) - (gls_type, ctx) + ctx gls_type (Lemmas.mk_hook hook); if Indfun_common.is_strict_tcc () then @@ -1360,12 +1360,11 @@ let com_terminate thm_name using_lemmas nb_args ctx hook = - let ctx = Univ.ContextSet.of_context ctx in let start_proof ctx (tac_start:tactic) (tac_end:tactic) = let (evmap, env) = Lemmas.get_current_context() in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) - (compute_terminate_type nb_args fonctional_ref, ctx) hook; + ctx (compute_terminate_type nb_args fonctional_ref) hook; ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref @@ -1374,7 +1373,7 @@ let com_terminate start_proof ctx tclIDTAC tclIDTAC; try let sigma, new_goal_type = build_new_goal_type () in - open_new_goal start_proof (Evd.universe_context_set sigma) + open_new_goal start_proof (Evd.evar_universe_context sigma) using_lemmas tcc_lemma_ref (Some tcc_lemma_name) (new_goal_type); @@ -1414,7 +1413,8 @@ let (com_eqn : int -> Id.t -> let equation_lemma_type = subst1 f_constr equation_lemma_type in (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) - (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty) + (Evd.evar_universe_context evmap) + equation_lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (by (Proofview.V82.tactic (start_equation f_ref terminate_ref @@ -1481,8 +1481,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let ctx = Evd.universe_context evm in - let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in + let ctx = Evd.evar_universe_context evm in + let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(Evd.universe_context evm) res in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in let relation = fst (*FIXME*)(interp_constr diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 8b9631b4b..d5aaf9df3 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -305,10 +305,10 @@ let empty_evar_universe_context = uctx_universes = Univ.initial_universes; uctx_initial_universes = Univ.initial_universes } -let evar_universe_context_from e c = +let evar_universe_context_from e = let u = universes e in {empty_evar_universe_context with - uctx_local = c; uctx_universes = u; uctx_initial_universes = u} + uctx_universes = u; uctx_initial_universes = u} let is_empty_evar_universe_context ctx = Univ.ContextSet.is_empty ctx.uctx_local && @@ -751,9 +751,10 @@ let empty = { effects = Declareops.no_seff; } -let from_env ?(ctx=Univ.ContextSet.empty) e = - { empty with universes = evar_universe_context_from e ctx } - +let from_env ?ctx e = + match ctx with + | None -> { empty with universes = evar_universe_context_from e } + | Some ctx -> { empty with universes = ctx } let has_undefined evd = not (EvMap.is_empty evd.undf_evars) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 3b58910e1..1393a33d3 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -117,6 +117,9 @@ val map_evar_info : (constr -> constr) -> evar_info -> evar_info (** {6 Unification state} **) +type evar_universe_context +(** The universe context associated to an evar map *) + type evar_map (** Type of unification state. Essentially a bunch of state-passing data needed to handle incremental term construction. *) @@ -128,7 +131,7 @@ val progress_evar_map : evar_map -> evar_map -> bool val empty : evar_map (** The empty evar map. *) -val from_env : ?ctx:Univ.universe_context_set -> env -> evar_map +val from_env : ?ctx:evar_universe_context -> env -> evar_map (** The empty evar map with given universe context, taking its initial universes from env. *) @@ -408,9 +411,6 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -(** The universe context associated to an evar map *) -type evar_universe_context - type 'a in_evar_universe_context = 'a * evar_universe_context val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 077057f3c..d3410ea75 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -25,9 +25,9 @@ let delete_proof = Proof_global.discard let delete_current_proof = Proof_global.discard_current let delete_all_proofs = Proof_global.discard_all -let start_proof (id : Id.t) str hyps c ?init_tac terminator = +let start_proof (id : Id.t) str ctx hyps c ?init_tac terminator = let goals = [ (Global.env_of_context hyps , c) ] in - Proof_global.start_proof id str goals terminator; + Proof_global.start_proof id str ctx goals terminator; let env = Global.env () in ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with @@ -118,8 +118,8 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic id sign ?(goal_kind = Global, false, Proof Theorem) typ tac = - start_proof id goal_kind sign typ (fun _ -> ()); +let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = + start_proof id goal_kind ctx sign typ (fun _ -> ()); try let status = by tac in let _,(const,univs,_) = cook_proof () in @@ -130,15 +130,16 @@ let build_constant_by_tactic id sign ?(goal_kind = Global, false, Proof Theorem) delete_current_proof (); raise reraise -let build_by_tactic env ?(poly=false) typ tac = +let build_by_tactic env ctx ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in - let ce, status, univs = build_constant_by_tactic id sign ~goal_kind:gk typ tac in + let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in let ce = Term_typing.handle_side_effects env ce in - let cb, se = Future.force ce.const_entry_body in + let (cb, ctx), se = Future.force ce.const_entry_body in assert(Declareops.side_effects_is_empty se); - cb, status, fst univs + assert(Univ.ContextSet.is_empty ctx); + cb, status, univs (**********************************************************************) (* Support for resolution of evars in tactic interpretation, including @@ -160,7 +161,7 @@ let solve_by_implicit_tactic env sigma evk = let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in (try let (ans, _, _) = - build_by_tactic env (evi.evar_concl, Evd.universe_context_set sigma) tac in - fst ans + build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in + ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 615866c6a..acf809a2b 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -56,7 +56,7 @@ val delete_all_proofs : unit -> unit type lemma_possible_guards = Proof_global.lemma_possible_guards val start_proof : - Id.t -> goal_kind -> named_context_val -> constr Univ.in_universe_context_set -> + Id.t -> goal_kind -> Evd.evar_universe_context -> named_context_val -> constr -> ?init_tac:unit Proofview.tactic -> Proof_global.proof_terminator -> unit @@ -148,13 +148,13 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit tactic. *) val build_constant_by_tactic : - Id.t -> named_context_val -> ?goal_kind:goal_kind -> - types Univ.in_universe_context_set -> unit Proofview.tactic -> - Entries.definition_entry * bool * Universes.universe_opt_subst Univ.in_universe_context + Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> + types -> unit Proofview.tactic -> + Entries.definition_entry * bool * Evd.evar_universe_context -val build_by_tactic : env -> ?poly:polymorphic -> - types Univ.in_universe_context_set -> unit Proofview.tactic -> - constr Univ.in_universe_context_set * bool * Universes.universe_opt_subst +val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> + types -> unit Proofview.tactic -> + constr * bool * Evd.evar_universe_context (** Declare the default tactic to fill implicit arguments *) diff --git a/proofs/proof.mli b/proofs/proof.mli index f2b64fb18..a77b74124 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -51,9 +51,9 @@ val proof : proof -> (*** General proof functions ***) -val start : Evd.evar_map -> (Environ.env * Term.types Univ.in_universe_context_set) list -> proof +val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof val dependent_start : Evd.evar_map -> Proofview.telescope -> proof -val initial_goals : proof -> (Term.constr * Term.types Univ.in_universe_context_set) list +val initial_goals : proof -> (Term.constr * Term.types) list (* Returns [true] if the considered proof is completed, that is if no goal remain to be considered (this does not require that all evars have been solved). *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 7c44f1500..410335b47 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -63,7 +63,7 @@ let _ = (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_universes = Universes.universe_opt_subst Univ.in_universe_context +type proof_universes = Evd.evar_universe_context type proof_object = { id : Names.Id.t; @@ -222,22 +222,22 @@ let disactivate_proof_mode mode = is (spiwack: for potential printing, I believe is used only by closing commands and the xml plugin); [terminator] is used at the end of the proof to close the proof. *) -let start_proof id str goals terminator = +let start_proof id str ctx goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; - proof = Proof.start (Evd.from_env (Global.env ())) goals; + proof = Proof.start (Evd.from_env ~ctx (Global.env ())) goals; endline_tactic = None; section_vars = None; strength = str; mode = find_proof_mode "No" } in push initial_state pstates -let start_dependent_proof id str goals terminator = +let start_dependent_proof id str ctx goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; - proof = Proof.dependent_start (Evd.from_env (Global.env ())) goals; + proof = Proof.dependent_start (Evd.from_env ~ctx (Global.env ())) goals; endline_tactic = None; section_vars = None; strength = str; @@ -269,54 +269,33 @@ let close_proof ?feedback_id ~now fpl = let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let fpl, univs = Future.split2 fpl in - let univsubst, make_body = + let universes = Future.force univs in + let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) + (Evd.evar_universe_context_subst universes) in + let make_body = if poly || now then - let make_usubst (usubst, uctx) = - let ctx, subst = - Universes.simplify_universe_context (Univ.ContextSet.of_context uctx) - in - let nf x = - let nf x = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst x in - Vars.subst_univs_level_constr subst (nf x) - in - let subst = - Univ.LMap.union usubst (Univ.LMap.map (fun v -> Some (Univ.Universe.make v)) subst) - in - let univsubst = (subst, Univ.ContextSet.to_context ctx) in - univsubst, nf - in - let make_body nf ctx t _octx ((c, _ctx), eff) = - let body = nf c and typ = nf t in + let make_body t ((c, _ctx), eff) = + let body = c and typ = nf t in let used_univs = Univ.LSet.union (Universes.universes_of_constr body) - (Universes.universes_of_constr typ) + (Universes.universes_of_constr typ) in - let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) used_univs in - let p = (body, Univ.ContextSet.empty),eff in + let ctx = Evd.evar_universe_context_set universes in + let ctx = Universes.restrict_universe_context ctx used_univs in let univs = Univ.ContextSet.to_context ctx in + let p = (body, Univ.ContextSet.empty), eff in (univs, typ), p - in - let make_body nf ctx t octx p = - Future.split2 (Future.chain ~pure:true p (make_body nf ctx t octx)) - in - let univsubst = - Future.chain ~pure:true univs make_usubst - in univsubst, make_body + in + fun t p -> + Future.split2 (Future.chain ~pure:true p (make_body t)) else - let ctx = - List.fold_left (fun acc (c, (t, octx)) -> - Univ.ContextSet.union octx acc) - Univ.ContextSet.empty initial_goals - in - let univs = Univ.ContextSet.to_context ctx in - let univsubst = (Univ.LMap.empty, univs) in - let make_body nf ctx t octx p = Future.from_val (univs, t), p in - Future.from_val (univsubst, fun x -> x), make_body + let univs = Evd.evar_context_universe_context universes in + fun t p -> + Future.from_val (univs, nf t), p in - let univsubst, nf = Future.force univsubst in let entries = - Future.map2 (fun p (c, (t, octx)) -> - let univstyp, body = make_body nf (snd univsubst) t octx p in + Future.map2 (fun p (c, t) -> + let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in { Entries. const_entry_body = body; @@ -329,11 +308,10 @@ let close_proof ?feedback_id ~now fpl = const_entry_polymorphic = poly; const_entry_proj = false}) fpl initial_goals in - { id = pid; entries = entries; persistence = strength; universes = univsubst }, + { id = pid; entries = entries; persistence = strength; universes = universes }, Ephemeron.get terminator -type closed_proof_output = Entries.proof_output list * - Universes.universe_opt_subst Univ.in_universe_context +type closed_proof_output = Entries.proof_output list * Evd.evar_universe_context let return_proof () = let { proof } = cur_pstate () in @@ -352,14 +330,12 @@ let return_proof () = str"variables still non-instantiated") in let eff = Evd.eval_side_effects evd in let evd = Evd.nf_constraints evd in - let subst = Evd.universe_subst evd in - let ctx = Evd.universe_context_set evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) let proofs = - List.map (fun (c, _) -> ((Evarutil.nf_evars_universes evd c, ctx), eff)) initial_goals in - proofs, (subst, Univ.ContextSet.to_context ctx) + List.map (fun (c, _) -> ((Evarutil.nf_evars_universes evd c, Univ.ContextSet.empty), eff)) initial_goals in + proofs, Evd.evar_universe_context evd let close_future_proof ~feedback_id proof = close_proof ~feedback_id ~now:false proof @@ -523,7 +499,7 @@ module V82 = struct let get_current_initial_conclusions () = let { pid; strength; proof } = cur_pstate () in let initial = Proof.initial_goals proof in - let goals = List.map (fun (o, (c, ctx)) -> c) initial in + let goals = List.map (fun (o, c) -> c) initial in pid, (goals, strength) end diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 1ad1cebf8..d5229c562 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -53,7 +53,7 @@ val give_me_the_proof : unit -> Proof.proof (i.e. an proof ending command) and registers the appropriate values. *) type lemma_possible_guards = int list list -type proof_universes = Universes.universe_opt_subst Univ.in_universe_context +type proof_universes = Evd.evar_universe_context type proof_object = { id : Names.Id.t; entries : Entries.definition_entry list; @@ -78,13 +78,13 @@ type closed_proof = proof_object * proof_terminator closing commands and the xml plugin); [terminator] is used at the end of the proof to close the proof. *) val start_proof : - Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types Univ.in_universe_context_set) list -> + Names.Id.t -> Decl_kinds.goal_kind -> Evd.evar_universe_context -> (Environ.env * Term.types) list -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between initial goals. *) val start_dependent_proof : - Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope -> + Names.Id.t -> Decl_kinds.goal_kind -> Evd.evar_universe_context -> Proofview.telescope -> proof_terminator -> unit (* Takes a function to add to the exceptions data relative to the @@ -95,8 +95,7 @@ val close_proof : (exn -> exn) -> closed_proof * Both access the current proof state. The formes is supposed to be * chained with a computation that completed the proof *) -type closed_proof_output = Entries.proof_output list * - Universes.universe_opt_subst Univ.in_universe_context +type closed_proof_output = Entries.proof_output list * Evd.evar_universe_context val return_proof : unit -> closed_proof_output val close_future_proof : feedback_id:Stateid.t -> diff --git a/proofs/proofview.ml b/proofs/proofview.ml index eaaa1f7c3..c8983700f 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -26,7 +26,7 @@ open Util type proofview = Proofview_monad.proofview open Proofview_monad -type entry = (Term.constr * Term.types Univ.in_universe_context_set) list +type entry = (Term.constr * Term.types) list let proofview p = p.comb , p.solution @@ -36,13 +36,12 @@ let proofview p = let init sigma = let rec aux = function | [] -> [], { solution = sigma; comb = []; } - | (env, (typ,ctx)) :: l -> + | (env, typ) :: l -> let ret, { solution = sol; comb = comb } = aux l in let (new_defs , econstr) = Evarutil.new_evar sol env typ in let (e, _) = Term.destEvar econstr in - let new_defs = Evd.merge_context_set Evd.univ_rigid new_defs ctx in let gl = Goal.build e in - let entry = (econstr, (typ, ctx)) :: ret in + let entry = (econstr, typ) :: ret in entry, { solution = new_defs; comb = gl::comb; } in fun l -> @@ -52,18 +51,17 @@ let init sigma = type telescope = | TNil - | TCons of Environ.env * Term.types Univ.in_universe_context_set * (Term.constr -> telescope) + | TCons of Environ.env * Term.types * (Term.constr -> telescope) let dependent_init = let rec aux sigma = function | TNil -> [], { solution = sigma; comb = []; } - | TCons (env, (typ, ctx), t) -> + | TCons (env, typ, t) -> let (sigma, econstr ) = Evarutil.new_evar sigma env typ in - let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let ret, { solution = sol; comb = comb } = aux sigma (t econstr) in let (e, _) = Term.destEvar econstr in let gl = Goal.build e in - let entry = (econstr, (typ, ctx)) :: ret in + let entry = (econstr, typ) :: ret in entry, { solution = sol; comb = gl :: comb; } in fun sigma t -> diff --git a/proofs/proofview.mli b/proofs/proofview.mli index c27e4ba1a..f959513d4 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -37,11 +37,11 @@ type entry (* Initialises a proofview, the argument is a list of environement, conclusion types, creating that many initial goals. *) -val init : Evd.evar_map -> (Environ.env * Term.types Univ.in_universe_context_set) list -> entry * proofview +val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview type telescope = | TNil - | TCons of Environ.env * Term.types Univ.in_universe_context_set * (Term.constr -> telescope) + | TCons of Environ.env * Term.types * (Term.constr -> telescope) (* Like [init], but goals are allowed to be depedenent on one another. Dependencies between goals is represented with the type @@ -57,7 +57,7 @@ val finished : proofview -> bool val return : proofview -> Evd.evar_map val partial_proof : entry -> proofview -> constr list -val initial_goals : entry -> (constr * types Univ.in_universe_context_set) list +val initial_goals : entry -> (constr * types) list val emit_side_effects : Declareops.side_effects -> proofview -> proofview (*** Focusing operations ***) diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 5f580bca5..e5cfeecdf 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -207,14 +207,14 @@ let compute_proof_name locality = function | None -> next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) -let save_remaining_recthms (locality,p,kind) body opaq i (id,((t_i,ctx_i),(_,imps))) = +let save_remaining_recthms (locality,p,kind) ctx body opaq i (id,(t_i,(_,imps))) = match body with | None -> (match locality with | Discharge -> let impl = false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum ((t_i,ctx_i),p,impl) in + let c = SectionLocalAssum ((t_i,ctx),p,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) | Local | Global -> @@ -224,7 +224,7 @@ let save_remaining_recthms (locality,p,kind) body opaq i (id,((t_i,ctx_i),(_,imp | Global -> false | Discharge -> assert false in - let ctx = Univ.ContextSet.to_context ctx_i in + let ctx = Univ.ContextSet.to_context ctx in let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) @@ -237,12 +237,12 @@ let save_remaining_recthms (locality,p,kind) body opaq i (id,((t_i,ctx_i),(_,imp match locality with | Discharge -> let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p - ~univs:(Univ.ContextSet.to_context ctx_i) body_i in + ~univs:(Univ.ContextSet.to_context ctx) body_i in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in (Discharge,VarRef id,imps) | Local | Global -> - let ctx = Univ.ContextSet.to_context ctx_i in + let ctx = Univ.ContextSet.to_context ctx in let local = match locality with | Local -> true | Global -> false @@ -326,7 +326,7 @@ let standard_proof_terminator compute_guard hook = let universe_proof_terminator compute_guard hook = let open Proof_global in function | Admitted -> - admit (hook (Univ.LMap.empty, Univ.UContext.empty)) (); + admit (hook Evd.empty_evar_universe_context) (); Pp.feedback Interface.AddedAxiom | Proved (is_opaque,idopt,proof) -> let proof = get_proof proof compute_guard @@ -338,31 +338,29 @@ let universe_proof_terminator compute_guard hook = save_anonymous_with_strength proof kind id end -let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook = +let start_proof id kind ctx ?sign c ?init_tac ?(compute_guard=[]) hook = let terminator = standard_proof_terminator compute_guard hook in let sign = match sign with | Some sign -> sign | None -> initialize_named_context_for_proof () in - !start_hook (fst c); - Pfedit.start_proof id kind sign c ?init_tac terminator + !start_hook c; + Pfedit.start_proof id kind ctx sign c ?init_tac terminator -let start_proof_univs id kind ?sign c ?init_tac ?(compute_guard=[]) hook = +let start_proof_univs id kind ctx ?sign c ?init_tac ?(compute_guard=[]) hook = let terminator = universe_proof_terminator compute_guard hook in let sign = match sign with | Some sign -> sign | None -> initialize_named_context_for_proof () in - !start_hook (fst c); - Pfedit.start_proof id kind sign c ?init_tac terminator + !start_hook c; + Pfedit.start_proof id kind ctx sign c ?init_tac terminator - -(* FIXME: forgetting about the universes here *) let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun (id,(t,_)) -> (id,fst t)) thms with + match List.map (fun (id,(t,_)) -> (id,t)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -370,11 +368,11 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun (id,(t,_)) n -> (id,n,fst t)) thms nl with + in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_proof_with_initialization kind recguard thms snl hook = +let start_proof_with_initialization kind ctx recguard thms snl hook = let intro_tac (_, (_, (ids, _))) = Tacticals.New.tclMAP (function | Name id -> Tactics.intro_mustbe_force id @@ -405,12 +403,13 @@ let start_proof_with_initialization kind recguard thms snl hook = if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) let body,opaq = retrieve_first_recthm ref in - List.map_i (save_remaining_recthms kind body opaq) 1 other_thms in + let ctx = Evd.evar_universe_context_set ctx in + List.map_i (save_remaining_recthms kind ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof id kind t ?init_tac (mk_hook hook) ~compute_guard:guard + start_proof id kind ctx t ?init_tac (mk_hook hook) ~compute_guard:guard let start_proof_com kind thms hook = let env0 = Global.env () in @@ -427,11 +426,9 @@ let start_proof_com kind thms hook = thms in let recguard,thms,snl = look_for_possibly_mutual_statements thms in let evd, nf = Evarutil.nf_evars_and_universes !evdref in - let ctxset = Evd.universe_context_set evd in - let thms = List.map (fun (n, (t, info)) -> (n, ((nf t, ctxset), info))) - thms - in - start_proof_with_initialization kind recguard thms snl hook + let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in + start_proof_with_initialization kind (Evd.evar_universe_context evd) + recguard thms snl hook (* Saving a proof *) diff --git a/stm/lemmas.mli b/stm/lemmas.mli index d0dd2d333..d5a4c709e 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -25,11 +25,11 @@ val call_hook : (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (types -> unit) -> unit -val start_proof : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types Univ.in_universe_context_set -> +val start_proof : Id.t -> goal_kind -> Evd.evar_universe_context -> ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit -val start_proof_univs : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types Univ.in_universe_context_set -> +val start_proof_univs : Id.t -> goal_kind -> Evd.evar_universe_context -> ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Proof_global.proof_universes -> unit declaration_hook) -> unit @@ -38,8 +38,8 @@ val start_proof_com : goal_kind -> unit declaration_hook -> unit val start_proof_with_initialization : - goal_kind -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> - (Id.t * (types Univ.in_universe_context_set * (Name.t list * Impargs.manual_explicitation list))) list + goal_kind -> Evd.evar_universe_context -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> + (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit val standard_proof_terminator : diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 9b600409a..f497b99d6 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -50,7 +50,8 @@ let optimize_non_type_induction_scheme kind dep sort ind = let ctx = if mib.mind_polymorphic then mib.mind_universes else Univ.UContext.empty in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in - let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ctxset env) (ind,u) dep sort in + let ectx = Evd.evar_universe_context_of ctxset in + let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in (c, Evd.evar_universe_context sigma), Declareops.no_seff let build_induction_scheme_in_type dep sort ind = @@ -61,7 +62,8 @@ let build_induction_scheme_in_type dep sort ind = in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in - let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ctxset env) (ind,u) dep sort in + let ectx = Evd.evar_universe_context_of ctxset in + let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in c, Evd.evar_universe_context sigma let rect_scheme_kind_from_type = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index da1475d7b..9cb22e5ea 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -304,10 +304,11 @@ open Coqlib let project_hint pri l2r r = let gr = Smartlocate.global_with_alias r in let env = Global.env() in - let c,ctx = Universes.fresh_global_instance env gr in - let t = Retyping.get_type_of env (Evd.from_env ~ctx env) c in + let sigma = Evd.from_env env in + let sigma, c = Evd.fresh_global env sigma gr in + let t = Retyping.get_type_of env sigma c in let t = - Tacred.reduce_to_quantified_ref env Evd.empty (Lazy.force coq_iff_ref) t in + Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in let sign,ccl = decompose_prod_assum t in let (a,b) = match snd (decompose_app ccl) with | [a;b] -> (a,b) @@ -320,6 +321,7 @@ let project_hint pri l2r r = let id = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in + let ctx = Evd.universe_context_set sigma in let c = Declare.declare_definition ~internal:Declare.KernelSilent id (c,ctx) in (pri,false,true,Auto.PathAny, Auto.IsGlobRef (Globnames.ConstRef c)) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index a10ad1e2b..d4f521054 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -194,7 +194,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = errorlabstrm "lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let pf = Proof.start Evd.empty [invEnv,(invGoal,universe_context_set sigma)] in + let pf = Proof.start (Evd.from_env ~ctx:(evar_universe_context sigma) invEnv) [invEnv,invGoal] in let pf = fst (Proof.run_tactic env ( tclTHEN intro (onLastHypId inv_op)) pf) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index b4b8d468c..477e5bcda 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -589,8 +589,9 @@ let solve_remaining_by by env prf = let evd' = List.fold_right (fun mv evd -> let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in - let c,_,_ = Pfedit.build_by_tactic env.env (ty,Univ.ContextSet.empty) (Tacticals.New.tclCOMPLETE tac) in - meta_assign mv (fst c (*FIXME*), (Conv,TypeNotProcessed)) evd) + let c,_,ctx' = Pfedit.build_by_tactic env.env (Evd.evar_universe_context evd) ty (Tacticals.New.tclCOMPLETE tac) in + let evd = Evd.set_universe_context evd ctx' in + meta_assign mv (c, (Conv,TypeNotProcessed)) evd) indep env.evd in { env with evd = evd' }, prf @@ -1236,7 +1237,8 @@ module Strategies = fail cs let inj_open hint = - (Evd.from_env ~ctx:hint.Autorewrite.rew_ctx (Global.env()), + let ctx = Evd.evar_universe_context_of hint.Autorewrite.rew_ctx in + (Evd.from_env ~ctx (Global.env()), (hint.Autorewrite.rew_lemma, NoBindings)) let old_hints (db : string) : strategy = @@ -1727,7 +1729,7 @@ let declare_projection n instance_id r = let build_morphism_signature m = let env = Global.env () in let m,ctx = Constrintern.interp_constr Evd.empty env m in - let sigma = Evd.from_env ~ctx:(Evd.evar_universe_context_set ctx) env in + let sigma = Evd.from_env ~ctx env in let t = Typing.type_of env sigma m in let cstrs = let rec aux t = @@ -1788,7 +1790,7 @@ let add_morphism_infer glob m n = let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in let instance = build_morphism_signature m in - let ctx = Univ.ContextSet.empty (*FIXME *) in + let ctx = Evd.empty_evar_universe_context (*FIXME *) in if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id (Entries.ParameterEntry @@ -1815,7 +1817,7 @@ let add_morphism_infer glob m n = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - Lemmas.start_proof instance_id kind (instance, ctx) hook; + Lemmas.start_proof instance_id kind ctx instance hook; ignore (Pfedit.by (Tacinterp.interp tac))) () let add_morphism glob binders m s n = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1d76f4afd..aafe6f2f7 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2060,8 +2060,7 @@ let _ = if has_type arg (glbwit wit_tactic) then let tac = out_gen (glbwit wit_tactic) arg in let tac = interp_tactic ist tac in - let ctx = Evd.universe_context_set sigma in - let prf = Proof.start sigma [env, (ty, ctx)] in + let prf = Proof.start sigma [env, ty] in let (prf, _) = try Proof.run_tactic env tac prf with Proof_errors.TacticFailure e as src -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 984e165d1..c7fc4197e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3823,8 +3823,9 @@ let abstract_subproof id gk tac = evd, ctx, nf concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in - let (const, safe, (subst, ctx)) = - try Pfedit.build_constant_by_tactic ~goal_kind:gk id secsign (concl, ctx) solve_tac + let ectx = Evd.evar_universe_context evd in + let (const, safe, ectx) = + try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx secsign concl solve_tac with Proof_errors.TacticFailure e as src -> (* if the tactic [tac] fails, it reports a [TacticFailure e], which is an error irrelevant to the proof system (in fact it @@ -3840,8 +3841,7 @@ let abstract_subproof id gk tac = let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in - let evd = Evd.merge_context_set Evd.univ_rigid evd (Univ.ContextSet.of_context ctx) in - let evd = Evd.merge_universe_subst evd subst in + let evd = Evd.set_universe_context evd ectx in let open Declareops in let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in let effs = cons_side_effects eff diff --git a/test-suite/bugs/opened/HoTT_coq_062.v b/test-suite/bugs/opened/HoTT_coq_062.v index e0ff5459c..7f1908f08 100644 --- a/test-suite/bugs/opened/HoTT_coq_062.v +++ b/test-suite/bugs/opened/HoTT_coq_062.v @@ -65,16 +65,17 @@ Definition e : Bool <~> Bool. admit. Defined. -Definition p `{Univalence} : Bool = Bool := path_universe e. +Definition p `{Univalence} : @paths Set Bool Bool := path_universe e. Theorem thm `{Univalence} : (forall A : Set, ((A -> False) -> False) -> A) -> False. intro f. Set Printing Universes. Set Printing All. + pose proof (apD f p). + pose(path_universe e). pose proof (apD f (path_universe e)). - cut `{Univalence}; intros. pose proof (apD f p). -Admitted. - (* ??? Toplevel input, characters 0-37: + admit. +Defined. (* ??? Toplevel input, characters 0-37: Error: Unable to satisfy the following constraints: In environment: diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index de0459089..0fbf0654f 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -641,11 +641,11 @@ let make_bl_scheme mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in - let ctx = Univ.ContextSet.empty (*FIXME univs *) in - let (ans, _, _) = Pfedit.build_by_tactic (Global.env()) (bl_goal, ctx) + let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in + let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx bl_goal (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec) in - ([|fst ans (*FIXME univs*)|], Evd.empty_evar_universe_context), eff + ([|ans|], ctx), eff let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme @@ -763,10 +763,11 @@ let make_lb_scheme mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in - let (ans, _, _) = Pfedit.build_by_tactic (Global.env()) (lb_goal,Univ.ContextSet.empty) + let ctx = Evd.empty_evar_universe_context in + let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in - ([|fst ans|], Evd.empty_evar_universe_context (* FIXME *)), eff + ([|ans|], ctx (* FIXME *)), eff let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme @@ -933,13 +934,14 @@ let make_eq_decidability mind = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in + let ctx = Evd.empty_evar_universe_context (* FIXME *)in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - let (ans, _, _) = Pfedit.build_by_tactic (Global.env()) - (compute_dec_goal (ind,u) lnamesparrec nparrec, Univ.ContextSet.empty) + let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx + (compute_dec_goal (ind,u) lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec) in - ([|fst ans (*FIXME*)|], Evd.empty_evar_universe_context (* FIXME *)), Declareops.no_seff + ([|ans|], ctx), Declareops.no_seff let eq_dec_scheme_kind = declare_mutual_scheme_object "_eq_dec" make_eq_decidability diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 07f4354b5..d888d6ffa 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -295,14 +295,14 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro | None -> [||], None, termtype in let hook = Lemmas.mk_hook hook in - let ctx = Evd.universe_context_set evm in + let ctx = Evd.evar_universe_context evm in ignore (Obligations.add_definition id ?term:constr typ ctx ~kind:(Global,poly,Instance) ~hook obls); id else (Flags.silently (fun () -> - Lemmas.start_proof id kind (termtype, Evd.universe_context_set evm) + Lemmas.start_proof id kind (Evd.evar_universe_context evm) termtype (Lemmas.mk_hook (fun _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) diff --git a/toplevel/command.ml b/toplevel/command.ml index 13696a17c..1f9d725b8 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -182,7 +182,7 @@ let do_definition ident k bl red_option c ctypopt hook = let obls, _, c, cty = Obligations.eterm_obligations env ident evd 0 c typ in - let ctx = Evd.universe_context_set evd in + let ctx = Evd.evar_universe_context evd in ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in @@ -912,7 +912,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp in - let ctx = Evd.universe_context_set !evdref in + let ctx = Evd.evar_universe_context !evdref in ignore(Obligations.add_definition recname ~term:evars_def evars_typ ctx evars ~hook) @@ -980,18 +980,18 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) = let interp_fixpoint l ntns = let (env,_,evd),fix,info = interp_recursive true l ntns in check_recursive true env evd fix; - (fix,Evd.universe_context_set evd,info) + (fix,Evd.evar_universe_context evd,info) let interp_cofixpoint l ntns = let (env,_,evd),fix,info = interp_recursive false l ntns in check_recursive false env evd fix; - fix,Evd.universe_context_set evd,info + fix,Evd.evar_universe_context evd,info let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (len,imps,_) -> (id,((t,ctx),(len,imps)))) fixnames fixtypes fiximps in + List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in @@ -999,7 +999,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe Option.map (List.map Proofview.V82.tactic) init_tac in Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) - (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + ctx (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in @@ -1010,6 +1010,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in + let ctx = Evd.evar_universe_context_set ctx in let ctx = Universes.restrict_universe_context ctx vars in let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in let ctx = Univ.ContextSet.to_context ctx in @@ -1025,7 +1026,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (len,imps,_) -> (id,((t,ctx),(len,imps)))) fixnames fixtypes fiximps in + List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in @@ -1033,7 +1034,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns Option.map (List.map Proofview.V82.tactic) init_tac in Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) - (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + ctx (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in @@ -1041,6 +1042,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in + let ctx = Evd.evar_universe_context_set ctx in let ctx = Univ.ContextSet.to_context ctx in ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx) fixnames fixdecls fixtypes fiximps); @@ -1109,7 +1111,7 @@ let do_program_recursive local p fixkind fixl ntns = Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl end in - let ctx = Evd.universe_context_set evd in + let ctx = Evd.evar_universe_context evd in let kind = match fixkind with | Obligations.IsFixpoint _ -> (local, p, Fixpoint) | Obligations.IsCoFixpoint -> (local, p, CoFixpoint) diff --git a/toplevel/command.mli b/toplevel/command.mli index e48a77000..4d1c74907 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -131,24 +131,24 @@ type recursive_preentry = val interp_fixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * Univ.universe_context_set * + recursive_preentry * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list val interp_cofixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * Univ.universe_context_set * + recursive_preentry * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : locality -> polymorphic -> - recursive_preentry * Univ.universe_context_set * + recursive_preentry * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : locality -> polymorphic -> - recursive_preentry * Univ.universe_context_set * + recursive_preentry * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 067b92554..fc1df9f00 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -324,8 +324,7 @@ type program_info = { prg_name: Id.t; prg_body: constr; prg_type: constr; - prg_ctx: Univ.universe_context_set; - prg_subst : Universes.universe_opt_subst; + prg_ctx: Evd.evar_universe_context; prg_obligations: obligations; prg_deps : Id.t list; prg_fixkind : fixpoint_kind option ; @@ -389,18 +388,18 @@ let _ = let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type -let get_body subst obl = +let get_body obl = match obl.obl_body with | None -> assert false - | Some (DefinedObl c) -> + | Some (DefinedObl c) -> let ctx = Environ.constant_context (Global.env ()) c in - let pc = subst_univs_fn_puniverses (Univ.level_subst_of subst) (c, Univ.UContext.instance ctx) in + let pc = (c, Univ.UContext.instance ctx) in DefinedObl pc | Some (TermObl c) -> - TermObl (subst_univs_fn_constr subst c) + TermObl c -let get_obligation_body expand subst obl = - let c = get_body subst obl in +let get_obligation_body expand obl = + let c = get_body obl in let c' = if expand && obl.obl_status == Evar_kinds.Expand then (match c with @@ -411,21 +410,19 @@ let get_obligation_body expand subst obl = | TermObl c -> c) in c' -let obl_substitution expand subst obls deps = +let obl_substitution expand obls deps = Int.Set.fold (fun x acc -> let xobl = obls.(x) in let oblb = - try get_obligation_body expand subst xobl + try get_obligation_body expand xobl with e when Errors.noncritical e -> assert false in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) deps [] -let subst_deps expand subst obls deps t = - let subst = Universes.make_opt_subst subst in - let osubst = obl_substitution expand subst obls deps in - Vars.subst_univs_fn_constr subst - (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) +let subst_deps expand obls deps t = + let osubst = obl_substitution expand obls deps in + (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let rec prod_app t n = match kind_of_term (strip_outer_cast t) with @@ -453,8 +450,7 @@ let replace_appvars subst = in map_constr aux let subst_prog expand obls ints prg = - let usubst = Universes.make_opt_subst prg.prg_subst in - let subst = obl_substitution expand usubst obls ints in + let subst = obl_substitution expand obls ints in if get_hide_obligations () then (replace_appvars subst prg.prg_body, replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type)) @@ -463,8 +459,8 @@ let subst_prog expand obls ints prg = (Vars.replace_vars subst' prg.prg_body, Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type)) -let subst_deps_obl subst obls obl = - let t' = subst_deps true subst obls obl.obl_deps obl.obl_type in +let subst_deps_obl obls obl = + let t' = subst_deps true obls obl.obl_deps obl.obl_type in { obl with obl_type = t' } module ProgMap = Map.Make(Id) @@ -528,9 +524,11 @@ let subst_body expand prg = let declare_definition prg = let body, typ = subst_body true prg in + let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) + (Evd.evar_universe_context_subst prg.prg_ctx) in let ce = - definition_entry ~types:typ ~poly:(pi2 prg.prg_kind) - ~univs:(Univ.ContextSet.to_context prg.prg_ctx) body + definition_entry ~types:(nf typ) ~poly:(pi2 prg.prg_kind) + ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) in progmap_remove prg; !declare_definition_ref prg.prg_name @@ -599,7 +597,7 @@ let declare_mutual_definition l = mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) - let ctx = Univ.ContextSet.to_context first.prg_ctx in + let ctx = Evd.evar_context_universe_context first.prg_ctx in let kns = List.map4 (!declare_fix_ref (local, poly, kind) ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) @@ -677,7 +675,7 @@ let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook obls, b in { prg_name = n ; prg_body = b; prg_type = reduce t; - prg_ctx = ctx; prg_subst = Univ.LMap.empty; + prg_ctx = ctx; prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; @@ -789,18 +787,19 @@ let rec string_of_list sep f = function (* Solve an obligation using tactics, return the corresponding proof term *) -let solve_by_tac name evi t poly subst ctx = +let solve_by_tac name evi t poly ctx = let id = name in - let concl = Universes.subst_opt_univs_constr subst evi.evar_concl in - (* spiwack: the status is dropped. MS: the ctx is dropped too *) - let (entry,_,(subst,ctx)) = Pfedit.build_constant_by_tactic - id ~goal_kind:(goal_kind poly) evi.evar_hyps (concl, ctx) (Tacticals.New.tclCOMPLETE t) in + let concl = evi.evar_concl in + (* spiwack: the status is dropped. *) + let (entry,_,ctx') = Pfedit.build_constant_by_tactic + id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in let entry = Term_typing.handle_side_effects env entry in let body, eff = Future.force entry.Entries.const_entry_body in assert(Declareops.side_effects_is_empty eff); + assert(Univ.ContextSet.is_empty (snd body)); Inductiveops.control_only_guard (Global.env ()) (fst body) (*FIXME ignoring the context...*); - (fst body), subst, entry.Entries.const_entry_universes + (fst body), ctx' let rec solve_obligation prg num tac = let user_num = succ num in @@ -811,12 +810,10 @@ let rec solve_obligation prg num tac = else match deps_remaining obls obl.obl_deps with | [] -> - let ctx = prg.prg_ctx in - let obl = subst_deps_obl prg.prg_subst obls obl in + let obl = subst_deps_obl obls obl in let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in - Lemmas.start_proof_univs obl.obl_name kind - (Universes.subst_opt_univs_constr prg.prg_subst obl.obl_type, ctx) - (fun (subst, ctx) -> Lemmas.mk_hook (fun strength gr -> + Lemmas.start_proof_univs obl.obl_name kind prg.prg_ctx obl.obl_type + (fun ctx' -> Lemmas.mk_hook (fun strength gr -> let cst = match gr with ConstRef cst -> cst | _ -> assert false in let obl = let transparent = evaluable_constant cst (Global.env ()) in @@ -836,13 +833,12 @@ let rec solve_obligation prg num tac = in let obls = Array.copy obls in let _ = obls.(num) <- obl in - let ctx = Univ.ContextSet.of_context ctx in let res = try update_obls - {prg with prg_body = Universes.subst_opt_univs_constr subst prg.prg_body; - prg_type = Universes.subst_opt_univs_constr subst prg.prg_type; - prg_ctx = Univ.ContextSet.union prg.prg_ctx ctx; - prg_subst = Univ.LMap.union prg.prg_subst subst} + {prg with prg_body = prg.prg_body; + prg_type = prg.prg_type; + prg_ctx = ctx' } + obls (pred rem) with e when Errors.noncritical e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e)) @@ -879,7 +875,7 @@ and solve_obligation_by_tac prg obls i tac = | None -> try if List.is_empty (deps_remaining obls obl.obl_deps) then - let obl = subst_deps_obl prg.prg_subst obls obl in + let obl = subst_deps_obl obls obl in let tac = match tac with | Some t -> t @@ -888,11 +884,12 @@ and solve_obligation_by_tac prg obls i tac = | Some t -> t | None -> snd (get_default_tactic ()) in - let t, subst, ctx = + let t, ctx = solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) prg.prg_subst prg.prg_ctx + (pi2 prg.prg_kind) prg.prg_ctx in - obls.(i) <- declare_obligation {prg with prg_subst = subst} obl t ctx; + let uctx = Evd.evar_context_universe_context ctx in + obls.(i) <- declare_obligation {prg with prg_ctx = ctx} obl t uctx; true else false with e when Errors.noncritical e -> @@ -1022,8 +1019,8 @@ let admit_prog prg = (fun i x -> match x.obl_body with | None -> - let x = subst_deps_obl prg.prg_subst obls x in - let ctx = Univ.ContextSet.to_context prg.prg_ctx in + let x = subst_deps_obl obls x in + let ctx = Evd.evar_context_universe_context prg.prg_ctx in let kn = Declare.declare_constant x.obl_name ~local:true (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural) in diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index bf186193a..9033b06a2 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -64,7 +64,7 @@ val set_proofs_transparency : bool -> unit (* true = All transparent, false = Op val get_proofs_transparency : unit -> bool val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> - Univ.universe_context_set -> + Evd.evar_universe_context -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> @@ -81,7 +81,7 @@ type fixpoint_kind = val add_mutual_definitions : (Names.Id.t * Term.constr * Term.types * (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list -> - Univ.universe_context_set -> + Evd.evar_universe_context -> ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(Term.constr -> Term.constr) -> diff --git a/toplevel/record.ml b/toplevel/record.ml index 97f7ec85b..b3c052f01 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -72,7 +72,7 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields def id t ps nots fs = let env0 = Global.env () in - let evars = ref (Evd.from_env ~ctx:(Univ.ContextSet.empty) env0) in + let evars = ref (Evd.from_env env0) in let _ = let error bk (loc, name) = match bk, name with |