diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 12 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 8 |
4 files changed, 5 insertions, 21 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 31a73db04f..6b503a0112 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -140,6 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let status = by tac in let _,(const,univs,_) = cook_proof () in Proof_global.discard_current (); + let univs = UState.demote_seff_univs const univs in const, status, univs with reraise -> let reraise = CErrors.push reraise in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 535ef2013d..167d6bda0d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -348,13 +348,9 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now nf t else t in - let used_univs_body = Univops.universes_of_constr body in - let used_univs_typ = Univops.universes_of_constr typ in - (* Universes for private constants are relevant to the body *) - let used_univs_body = - List.fold_left (fun acc (us,_) -> Univ.LSet.union acc us) - used_univs_body (Safe_typing.universes_of_private eff) - in + let env = Global.env () in + let used_univs_body = Univops.universes_of_constr env body in + let used_univs_typ = Univops.universes_of_constr env typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = UState.const_univ_entry ~poly initial_euctx in @@ -362,7 +358,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now (* For vi2vo compilation proofs are computed now but we need to complement the univ constraints of the typ with the ones of the body. So we keep the two sets distinct. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx_body = UState.restrict ctx used_univs in let univs = UState.check_mono_univ_decl ctx_body universe_decl in (initunivs, typ), ((body, univs), eff) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a8ec4d8ca3..cab8d7b52a 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -102,9 +102,6 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls -let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c -let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c - (********************************************) (* Definition of the most primitive tactics *) (********************************************) @@ -223,8 +220,6 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d9496d2b4f..e0fb8fbc5d 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,9 +12,7 @@ open Environ open EConstr open Proof_type open Redexpr -open Pattern open Locus -open Ltac_pretype (** Operations for handling terms under a local typing context. *) @@ -79,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool - - (** {6 The most primitive tactics. } *) val refiner : rule -> tactic @@ -138,8 +132,6 @@ module New : sig val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr val pf_compute : 'a Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr end |