diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 9 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 4 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 |
5 files changed, 12 insertions, 10 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 613581ade7..285240872e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -230,8 +230,7 @@ let hyp_of_move_location = function | MoveBefore id -> id | _ -> assert false -let move_hyp sigma toleft (left,declfrom,right) hto = - let env = Global.env() in +let move_hyp env sigma toleft (left,declfrom,right) hto = let test_dep d d2 = if toleft then occur_var_in_decl env sigma (NamedDecl.get_id d2) d @@ -280,11 +279,11 @@ let move_hyp_in_named_context env sigma hfrom hto sign = let open EConstr in let (left,right,declfrom,toleft) = split_sign env sigma hfrom hto (named_context_of_val sign) in - move_hyp sigma toleft (left,declfrom,right) hto + move_hyp env sigma toleft (left,declfrom,right) hto -let insert_decl_in_named_context sigma decl hto sign = +let insert_decl_in_named_context env sigma decl hto sign = let open EConstr in - move_hyp sigma false ([],decl,named_context_of_val sign) hto + move_hyp env sigma false ([],decl,named_context_of_val sign) hto (**********************************************************************) diff --git a/proofs/logic.mli b/proofs/logic.mli index 9db54732bb..2cad278e10 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -75,6 +75,6 @@ val convert_hyp : bool -> Environ.named_context_val -> evar_map -> val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location -> Environ.named_context_val -> Environ.named_context_val -val insert_decl_in_named_context : Evd.evar_map -> +val insert_decl_in_named_context : Environ.env -> Evd.evar_map -> EConstr.named_declaration -> Id.t move_location -> Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index de151fb6e5..25cf789193 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -347,8 +347,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now not (Safe_typing.empty_private_constants = eff)) in let typ = if allow_deferred then t else nf t in - let used_univs_body = Univops.universes_of_constr body in - let used_univs_typ = Univops.universes_of_constr typ in + let used_univs_body = Vars.universes_of_constr body in + let used_univs_typ = Vars.universes_of_constr typ in if allow_deferred then let initunivs = UState.const_univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 5d1faf1465..388bf8efb5 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -68,7 +68,10 @@ 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 (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) +let pf_global gls id = + let env = pf_env gls in + let sigma = project gls in + Evd.fresh_global env sigma (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 diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 3432ad4afa..f302960870 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -34,7 +34,7 @@ val pf_hyps_types : goal sigma -> (Id.t * types) list val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list -val pf_global : goal sigma -> Id.t -> constr +val pf_global : goal sigma -> Id.t -> evar_map * constr val pf_unsafe_type_of : goal sigma -> constr -> types val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types |