diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 19 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 10 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 8 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 |
8 files changed, 22 insertions, 25 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index aeaf16723b..450fcddfde 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -13,8 +13,8 @@ open CErrors open Util open Names open Nameops -open Term open Termops +open Constr open Namegen open Environ open Evd diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 209104ac32..38ed63c23d 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -10,7 +10,7 @@ open Util open Names -open Term +open Constr open Termops open Evd open EConstr diff --git a/proofs/logic.ml b/proofs/logic.ml index 4934afa837..218b2671ec 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -481,7 +481,7 @@ and mk_arggoals sigma goal goalacc funty allargs = let env = Goal.V82.env sigma goal in raise (RefinerError (env,sigma,CannotApply (t, harg))) in - Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs + Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs and mk_casegoals sigma goal goalacc p c = let env = Goal.V82.env sigma goal in diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 805635dfa4..7b79732249 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -24,7 +24,7 @@ open Decl_kinds proof of mutually dependent theorems) *) val start_proof : - Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> + Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> ?init_tac:unit Proofview.tactic -> Proof_global.proof_terminator -> unit diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 842003bc86..3abdd129e4 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -78,9 +78,11 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * + | Proved of opacity_flag * Misctypes.lident option * proof_object @@ -95,7 +97,7 @@ type pstate = { proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; - universe_decl: Univdecls.universe_decl; + universe_decl: UState.universe_decl; } type t = pstate list @@ -236,13 +238,6 @@ let activate_proof_mode mode = let disactivate_current_proof_mode () = CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) -let default_universe_decl = - let open Misctypes in - { univdecl_instance = []; - univdecl_extensible_instance = true; - univdecl_constraints = Univ.Constraint.empty; - univdecl_extensible_constraints = true } - (** [start_proof sigma id pl str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -251,7 +246,7 @@ let default_universe_decl = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -let start_proof sigma id ?(pl=default_universe_decl) str goals terminator = +let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; @@ -263,7 +258,7 @@ let start_proof sigma id ?(pl=default_universe_decl) str goals terminator = universe_decl = pl } in push initial_state pstates -let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator = +let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; @@ -342,7 +337,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now normalise them for the kernel. *) let subst_evar k = Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in - let nf = Universes.nf_evars_and_universes_opt_subst subst_evar + let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst universes) in let make_body = if poly || now then diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index bf35fd6599..0141cacb9e 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -48,10 +48,12 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * + | Proved of opacity_flag * Misctypes.lident option * proof_object type proof_terminator @@ -69,14 +71,14 @@ val apply_terminator : proof_terminator -> proof_ending -> unit evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) val start_proof : - Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl -> + Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between initial goals. *) val start_dependent_proof : - Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> + Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> unit (** Update the proofs global environment after a side-effecting command @@ -128,7 +130,7 @@ val set_used_variables : val get_used_variables : unit -> Context.Named.t option (** Get the universe declaration associated to the current proof. *) -val get_universe_decl : unit -> Univdecls.universe_decl +val get_universe_decl : unit -> UState.universe_decl module V82 : sig val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 6fb4119387..03ebc32759 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open EConstr open Declarations open Globnames @@ -92,9 +92,9 @@ let cache_strategy (_,str) = let subst_strategy (subs,(local,obj)) = local, - List.smartmap + List.Smart.map (fun (k,ql as entry) -> - let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in + let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in if ql==ql' then entry else (k,ql')) obj @@ -263,7 +263,7 @@ let subst_mps subst c = EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) let subst_red_expr subs = - Miscops.map_red_expr_gen + Redops.map_red_expr_gen (subst_mps subs) (Mod_subst.subst_evaluable_reference subs) (Patternops.subst_pattern subs) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index c1d69dfc54..092bb5c276 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -75,7 +75,7 @@ let pf_ids_set_of_hyps gls = let pf_get_new_id id gls = next_ident_away id (pf_ids_set_of_hyps gls) -let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) +let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in |