diff options
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 3d734d3a66..f2241e78d2 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -773,7 +773,7 @@ let interp_may_eval f ist env sigma = function function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> - str"interpretation of term " ++ pr_glob_constr_env env (fst c))); + str"interpretation of term " ++ pr_glob_constr_env env sigma (fst c))); Exninfo.iraise reraise (* Interprets a constr expression possibly to first evaluate *) @@ -1667,10 +1667,10 @@ and interp_atomic ist tac : unit Proofview.tactic = (k,(make ?loc f))) cb in let sigma,tac = match cl with - | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l - | Some cl -> - let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in - sigma, Tactics.apply_delayed_in a ev id l cl in + | [] -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l + | cl -> + let sigma,cl = List.fold_left_map (interp_in_hyp_as ist env) sigma cl in + sigma, List.fold_right (fun (id,ipat) -> Tactics.apply_delayed_in a ev id l ipat) cl Tacticals.New.tclIDTAC in Tacticals.New.tclWITHHOLES ev tac sigma end end @@ -2099,6 +2099,7 @@ let interp_pre_ident ist env sigma s = let () = register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n)); + register_interp0 wit_nat_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n)); register_interp0 wit_smart_global (lift interp_reference); register_interp0 wit_ref (lift interp_reference); register_interp0 wit_pre_ident (lift interp_pre_ident); |