update in delayed_updating and ground

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / names.txt

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/names.txt b/matita/matita/contribs/lambdadelta/delayed_updating/names.txt
index cd980b56895087381b228a8fc0cb3c1955f4d0c1..715cb268e31b0055130c42ac5c27ba0de6d41b30 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/names.txt
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/names.txt
@@ -6,5 +6,6 @@ METAVARIABLES
   h, k      : reference index by depth
   l         : label
   m, n      : natural number
+  o         : option
   p, q, r, s: path
   t, u, v, w: term