X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ffr2_map.ma;h=a1f2f4d4e8d69d7d88cc1a3d274d3d7512d44773;hb=12dc655b7f5321b33b93a310d53e23e60e090caa;hp=3de9abeb3e22fe3fb3adb08f1cea561f949ddcba;hpb=dd41efaab7f147d5673cc30a27d36375f9b52c9d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma
index 3de9abeb3..a1f2f4d4e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/diamond_0.ma".
+include "ground/notation/functions/element_e_0.ma".
 include "ground/notation/functions/semicolon_3.ma".
 include "ground/arith/nat.ma".
 
@@ -21,14 +21,15 @@ include "ground/arith/nat.ma".
 (*** mr2 *)
 inductive fr2_map: Type[0] :=
 (*** nil2 *)
-  | fr2_nil : fr2_map
+| fr2_empty: fr2_map
 (*** cons2 *)
-  | fr2_cons: nat → nat → fr2_map → fr2_map.
+| fr2_lcons: nat → nat → fr2_map → fr2_map
+.
 
 interpretation
-  "nil (finite relocation maps with pairs)"
-  'Diamond = (fr2_nil).
+  "empty (finite relocation maps with pairs)"
+  'ElementE = (fr2_empty).
 
 interpretation
-  "cons (finite relocation maps with pairs)"
-  'Semicolon d h f = (fr2_cons d h f).
+  "left cons (finite relocation maps with pairs)"
+  'Semicolon d h f = (fr2_lcons d h f).