1) CicNotationPres.render: type changed to make it more general (no
dependency on the Hashtbl) and URI/REFERENCE agnostic.
A compatibility function CicNotationPres.lookup_uri is provided to
easily map the (old) Hashtbl to the (new) lookup function.
2) user interface partially changed to render NG objects in the CicBrowser
and to follow NG hyperlinks
3) New CicNotationPt entries NRef (similar to Uri) and NRefPattern
(similar to UriPattern) to avoid hijacking the old Uris (actually,
uris + xpointers) to also hold new references.
This allows to properly implement notation (for NG) and to properly
handle hyperlinks.
4) all remaining Warnings for unused variables fixed (in some way or
another, hopefully the correct one)
5) GrafiteEngine, NQed: the height of an object is now recomputed just
before putting it in the environment. This fixes all the bugs related
to reduction.
6) GrafiteParser/LexiconEngine: both old URIs and new references are now
allowed in NG terms and in notations
7) ng_cic_content: rendering functions now return an "id |-> reference" table
to correctly implement MathML hrefs
8) NReference: new compare function
9) NCicUntrusted: new height_of_obj_kind function (to be used in GrafiteEngine)
10) OCic2NCic: new reference_of_oxuri function to map old uris + xpointers
into new references
11) bug fixed: after the commit by Enrico that starts using the extensible
PTS, the old-to-new objects translations used to map Type into "Type" which
was not declared. Type is now mapped into Type[0] and Type (as a "notation")
is now a synonim of Type[0] (only during parsing for now)
12) bug fixed: after the commit by Enrico that cleans up terms for
alpha-conversion and dummy products, the test in NCicTypeChecker that
verifies the consistency of left parameters in constructor --- that used
to do that NOT up to alpha-conversion --- used to fail when dummy products
were found. The test is now relaxed to include alpha-conversion.
13) bug fixed: NCicTypeChecker did not verify that a .dec reference pointed to
an axiom and that a .def reference did not point to an axiom. Fixed.