X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fchanges.tbl;fp=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fchanges.tbl;h=d25be28c73af8cf23fdef1adb73dd3df1f08a9eb;hb=9554ed555d9c744d7dfb787ccdaa6fc63eb6ba10;hp=0000000000000000000000000000000000000000;hpb=ba7b8553850e4a33cf8607b07758392230d9ed40;p=helm.git

diff --git a/helm/www/lambdadelta/web/home/changes.tbl b/helm/www/lambdadelta/web/home/changes.tbl
new file mode 100644
index 000000000..d25be28c7
--- /dev/null
+++ b/helm/www/lambdadelta/web/home/changes.tbl
@@ -0,0 +1,118 @@
+name "changes"
+
+table {
+  class "gray"
+  [ "version" [ "aspect" [ "" "changes" ]]
+  ]
+
+  class "orange"
+  [ { "λδ-2B" + "(unreleased)" * }
+    {
+     [ [{ "equivalences" * }]
+       { "+" "+" "+" "-" }
+       { "equivalence for full rt-reduction (terms)"
+         "equivalence for whd rt-reduction (terms)"
+         "equivalence for extended rt-reduction (terms, referred lenvs, closures)"
+         "syntactic equivalence (closures) removed"
+       }
+     ]
+     [ [{ "weights" * }]
+       { "+" }
+       { "switch in primitive order relations for closures to enable the exclusion binder"
+       }
+     ]
+     [ [{ "relocation" * }]
+       { "" }
+       { ""
+       }
+     ]
+     [ [{ "syntax" * }]
+       { "+" }
+       { "exclusion binder for lenvs"
+       }
+     ]
+     [ [{ "ground" * }]
+       { "+" "*" "+" "-" }
+       { "rt-transition counters"
+         "generic reference transforming maps as streams of non-negative integers" 
+         "extensional equality, labelled transitive closures and streams"
+         "non-negative integers with infinity removed"
+       }
+     ]
+    }
+  ]
+
+  class "orange"
+  [ { "λδ-2A" + "(October 2014)" * }
+    {
+     [ [{ "equivalences" * }]
+       { "+" }
+       { "syntactic equivalence (selected lenvs, referred lenvs, closures)"
+       }
+     ]
+     [ [{ "weights" * }]
+       { "*" "-" }
+       { "primitive order relations for closures"
+         "complex weight (terms) removed"
+       }
+     ]
+     [ [{ "relocation" * }]
+       { "-" }
+       { "level update functions removed"
+       }
+     ]
+     [ [{ "syntax" * }]
+       { "+" "+" "+" "-" "-" }
+       { "polarized binders for terms"
+         "non-negative integer global references for terms"
+         "syntactic support for genvs with typed abstraction, abbreviation"
+         "numbered sorts, application, type annotation removed from lenvs"
+         "exclusion binder removed from terms and lenvs"
+       }
+     ]
+     [ [{ "ground" * }]
+       { "+" "+" }
+       { "lists and non-negative integers with infinity"
+         "library extension for transitive closures and booleans"
+       }
+     ]
+    }
+  ]
+
+  class "red"
+  [ { "λδ-1A" + "(November 2006)" * }
+    {
+     [ [{ "equivalences" * }]
+       { "" }
+       { "equivalence for outer reduction (terms)"
+       }
+     ]
+     [ [{ "weights" * }]
+       { "" "" "" }
+       { "order relations (terms, lenvs, closures) based on weights" 
+         "simple weights (terms, lenvs, closures)"
+         "complex weight (terms)"
+       }
+     ]
+     [ [{ "relocation" * }]
+       { "" }
+       { "level update functions"
+       }
+     ]
+     [ [{ "syntax" * }]
+       { "" "" }
+       { "lenvs with non-negative integer sorts, application, typed abstraction, abbreviation, exclusion, type annotation"
+         "terms with non-negative integer sorts and local references, application, typed abstraction, abbreviation, exclusion, type annotation" }
+     ]
+     [ [{ "ground" * }]
+       { "" "" }
+       { "finite reference transforming maps as compositions of basic ones"
+         "library extension for logic and non-negative integers"
+       }
+     ]
+    }
+  ]
+
+}
+
+class "center" { 2 }