diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 8 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index da4a50b674..cfdaac710b 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -217,13 +217,13 @@ module Mlenv = struct (* Adding a type with no [Tvar], hence no generalization needed. *) - let push_type {env=e;free=f} t = - { env = (0,t) :: e; free = find_free f t} + let push_type mle t = + { env = (0,t) :: mle.env; free = find_free mle.free t} (* Adding a type with no [Tvar] nor [Tmeta]. *) - let push_std_type {env=e;free=f} t = - { env = (0,t) :: e; free = f} + let push_std_type mle t = + { env = (0,t) :: mle.env; free = mle.free} end diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 54d7c310aa..da95869abb 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1180,7 +1180,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l) | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) | TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v) - | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) + | TacSelect (sel, tac) -> Goal_select.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias {loc; v=(s,l)} -> let alias = Tacenv.interp_alias s in |