diff options
| author | Pierre-Marie Pédrot | 2017-09-04 19:14:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-04 19:20:23 +0200 |
| commit | 567435828772e53327bacf7464291a5759c23831 (patch) | |
| tree | 383e7ba91b9b119cb1fc281fc36bcc38ca82e582 /src/tac2core.ml | |
| parent | d80e854d6827252676c2c504bb3108152a94d629 (diff) | |
Better backtraces for a few datatypes.
Diffstat (limited to 'src/tac2core.ml')
| -rw-r--r-- | src/tac2core.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 17fa7c28f4..e4bd80adc8 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -930,9 +930,13 @@ let () = let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in GlbVal tac, gtypref t_unit in - let interp _ tac = + let interp ist tac = + let ist = { ist with env_ist = Id.Map.empty } in + let lfun = Tac2interp.set_env ist Id.Map.empty in + let ist = Ltac_plugin.Tacinterp.default_ist () in (** FUCK YOU API *) - (Obj.magic Ltac_plugin.Tacinterp.eval_tactic tac : unit Proofview.tactic) >>= fun () -> + let ist = { ist with API.Geninterp.lfun = (Obj.magic lfun) } in + (Obj.magic Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) >>= fun () -> return v_unit in let subst s tac = Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac in |