diff options
| author | Hugo Herbelin | 2018-10-09 19:47:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-14 13:27:34 +0200 |
| commit | 405a80db00537b5ccfb3b8655cd7baf61e890b20 (patch) | |
| tree | 3b09bf5dc63a3ae256e4c0908ce0012a52b7ccfd | |
| parent | 3a552450ddcdf96ef5b12be19ad67207697d298c (diff) | |
Passing env functionally in move_hyp and insert_decl_in_named_context.
| -rw-r--r-- | proofs/logic.ml | 9 | ||||
| -rw-r--r-- | proofs/logic.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
3 files changed, 6 insertions, 7 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/tactics/tactics.ml b/tactics/tactics.ml index 9ec3e203cc..18ddc9318d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -451,7 +451,7 @@ let internal_cut_gen ?(check=true) dir replace id t = if replace then let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in - let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in + let sign' = insert_decl_in_named_context env sigma (LocalAssum (id,t)) nexthyp sign' in sign',t,concl,sigma else (if check && mem_named_context_val id sign then |