aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
authorHugo Herbelin2014-12-07 12:47:08 +0100
committerHugo Herbelin2014-12-07 15:18:48 +0100
commitfa906a5137058cf12444c70b76908b959012ce6d (patch)
tree3d7075a34b8f11b17c810edb1fe2e109e67b178a /intf
parent3af8f3e522bdf2bd103bb437c65ad79ae04ac9c3 (diff)
Improved tracking of the origin of evars.
Diffstat (limited to 'intf')
-rw-r--r--intf/evar_kinds.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index e8281e07bb..f77fc5a6ab 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -28,3 +28,4 @@ type t =
| ImpossibleCase
| MatchingVar of bool * Id.t
| VarInstance of Id.t
+ | SubEvar of t