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 /tactics | |
| parent | 3a552450ddcdf96ef5b12be19ad67207697d298c (diff) | |
Passing env functionally in move_hyp and insert_decl_in_named_context.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |