Useless code removed.

Useless code removed.

Case-sensitive fixes.

a few missing ~subst added to whd

coercions are there, but not heavily tested

if todo_dom was [] disambiguation was performed twice

still commented, but benchmarks the new/old disambigution process

disambiguation takes ~mk_localization_tbl and not ~localization_tbl, thus can
create the hashtable when needed (after every interpretation)

raise failure instead of uncertain if two terms are meta closed

Fixes:
 - new letin interpretation in nCicDisambiguation fixed to not swap arguments
 - new refiner raises good exception in case a sort in not such
 - reference raise good exception instead of assert false
Improvements:
 - new disambiguation attached
 - constructor -> indty function in reference

housekeeping:
- unused functions removed from Enviconment
- unused file disambiguatePp removed
- disambiguation callbacks pushed down to Disambiguate
  from MultiPassDisambiguator

Bug fixed: pretty-printing of aliases when the OK button is pressed in the
ambiguous error window.

The aliases and multi_aliases in the lexicon status are now
LexiconAst.alias_spec (they used to be DisambiguateTypes.codomain_item).
Benefit: it is now possible to use the very same set of aliases both for the
new and old terms. Moreover, this commits simplifies quite a bit of code.

Known bugs: when clicking the "OK" button in the error message disambiguation
window, an assertion is often raised. When the assertion is not raised, the
set of aliases that are printed are not syntactically/semantically correct.

improved interface for brgEnvironment

log facility, initial environment for basic_rg

- we updated some preambles to match that of nUri.ml
- the transformation to from "meta" to "basic_rg" is now working

...

...

0.5.6 almost ok

0.5.6

we start a kernel for the version "basic with reverse indexes and global
references"

all done

more ex and more notation

better doc

rt.op and check.opt removed from Makefile

natural deduction support for lemmas with premises

lambda-delta/toplevel: improved transformation from automath (20 secs gained)
                       bug fix in the default arguments specification
       reverse indexes are now supported
transcript: unused parser productions removed

cicDischarge: final fixup. Now correctly processes Coq/Init/Logic.mma :)
              We handle missing abstractions in MutCase output type
procedural/Coq: we removed the depence from legacy

ng_disambiguation ng_kernel ng_refiner disambiguation: svn:ignore fixed
hExtlib: the map of list_findopt takes the position in the list (starts at 0)
cicRefine, acic2astMatcher, grafiteEngine: updated accordingly
cicUtil cicDischarge: bug fixes
cicSubstitution: new function lift_map for non-linear relocation
proceduralOptimizer: initial support for contrlling critical optimizations

it works!

new disambiguator almost attached

\forall x:?. and \forall x. both generate a meta for a type

metas for terms have height 3

...

...

virtualbox guide almost ok

...

...

...

...

...

New modules stack:
grafiteDisambiguator | cicDisambiguator |
                                        | multiPassDisambiagutor |disambiguate
                       nCicDisambiguator|

cic_disambiguation splitted into disambiguation and cic_disambiguation

disambiguate.ml splitted into disambiguate.ml and cicDisambiguate.ml

1. grafiteDisambiguator => multiPassDisambiguator
2.

new kernel is compiled since the META of grafite_parser depends on the META of ng_disambiguation

...

notation now digests Cic.Cast, not sure the precedence level is handled correctly

disambiguation should not fail if the new refiner fails

...

Re-added exception, just for now (debugging).

almost done

disambiguation even more abstracted

...

cicUtil: we moved here pp_term from proceduralHelpers
cicDischarge: some bugs fixed
transcript: we now support explicit declaration of dependences
procedural/Coq: we added an explicit dependence to Init/Prelude where needed

...

...

...

...

...

more on the livecd in the manual

....

...

formal topologies

fix some non tex symbols

symbolic links to use the uri manager from ng_kernel

print an error message if graphviz is not found

if gnome-help is not installed, prints an error message

better manual generation

...

one more lazy/loc

according to camlp5 sources, the dummy loc should be 0,0 and not -1,-1

loc * lazy string -> (loc * string) lazy

disambiguation now returns and takes in input the substitution

...

...

...

...

...

dama almost ok

...

...

reverted

dama into the library

x2sx declared as coercion and used when possible

renaming

...

0.5.5

...

...

exercises ready

all ex done

...

....

fixed

removed some printings

commented out unfinished proof

removed some printings

better spacing

apply rule (lem EM) works