update in ground

[helm.git] / matita / matita / predefined_virtuals.ml

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 09bcabd573932f74ae77e20f153343f2564ac66b..67c3571a48f954de4bd368b4c8b559d542c2ceb7 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1521,7 +1521,7 @@ let predefined_classes = [
  ["⇕"; "⇳"; "⬍"; "↕"; ];
  ["↔"; "⇔"; "⬄"; "⬌"; ] ; 
  ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ;
- ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ];
+ ["_"; "â\86\93"; "â\86\99"; "â\87£"; "â\87\83"; "â\87\82"; "â\8e½"; "â\8e¼"; "â\8e»"; "â\8eº"; ];
  ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
  ["("; "❨"; "❪"; "❲"; "（"; ];
  [")"; "❩"; "❫"; "❳"; "）"; ];