aboutsummaryrefslogtreecommitdiff
path: root/src/tac2interp.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-08-29 18:17:19 +0200
committerPierre-Marie Pédrot2017-08-29 18:26:41 +0200
commit31e686c2904c3015eaec18ce502d4e8afe565850 (patch)
treebb4a3d41d1a8352049b9a60d00247c4d5d1efdda /src/tac2interp.ml
parent94397f6e022176a29add6369f0a310b1d7decf62 (diff)
Rolling our own dynamic types for Ltac2.
This prevents careless confusions with generic arguments from Coq.
Diffstat (limited to 'src/tac2interp.ml')
-rw-r--r--src/tac2interp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 691c795502..3be95ac828 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -23,7 +23,7 @@ let () = register_handler begin function
| _ -> raise Unhandled
end
-let val_exn = Geninterp.Val.create "ltac2:exn"
+let val_exn = Tac2dyn.Val.create "ltac2:exn"
type environment = valexpr Id.Map.t