From 16f6bb96f5b619370e67700fbf4aae5abef05c94 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 30 Jun 2014 17:46:45 +0000
Subject: [PATCH] some additions and corrections ...

---
 matita/matita/contribs/lambdadelta/basic_2/names.txt | 4 ++--
 matita/matita/predefined_virtuals.ml                 | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt
index 9a3e5d490..328d64e87 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/names.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt
@@ -16,7 +16,7 @@ T,U,V,W: term
 X,Y,Z  : reserved: transient objet denoted by a capital letter
 
 a,b    : binder polarity
-c      : reserved: future use (lambda_delta 3)
+c      : reserved: future use (\lambda\delta 3)
 d      : relocation depth
 e      : relocation height
 f      :
@@ -30,7 +30,7 @@ o      :
 p,q    : global reference position
 r      : reduction kind parameter (true = ordinary, false = extended)
 s      : local dropping kind parameter (true = general, false = restricted)
-t,u    : local reference position level (de Bruijn's)
+t,u    : local reference position level (de Bruijn's) (RTM)
 v,w    :
 x,y,z  : reserved: transient objet denoted by a small letter
 
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 0a1135cb4..643f7c5ef 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1511,7 +1511,7 @@ let predefined_classes = [
  ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ];
  ["+"; "⊞"; ];
  ["-"; "÷"; "⊢"; "⊩"; "⊟"; ];
- ["="; "≝"; "⊜"; "≡"; "≃"; "≈"; "≅"; "≐"; "≑"; "≚"; "≙"; "⌆"; ];  
+ ["="; "≝"; "≡"; "⩬"; "≂"; "≃"; "≈"; "≅"; "≐"; "≑"; "≚"; "≙"; "⌆"; "⊜"; ];  
  ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
  ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "➤"; "➸"; "⇉"; "⥰"; ] ;
  ["^"; "↑"; ] ;
-- 
2.39.2