...

...

...

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

missing subst added, now apply rule is probably enough to replace apply

New bug.

no more prove in palette

fixed or-in-left

fixed not-e

Another bug.

This commit shows a bug.

almost ready

rules fixed

make all/clean implemented

housekeeping

housekeeping

house keeping

disambiguation can use a goal as hint for the expected type

natural deduction palette

test 4 luo

...

better names

disambiguation for ng terms almost there

some new exports

new meta added for ng_disambiguation

exported disambiguate_thing

occurr check fixed

more printings

last fixes

1. data structure for lables is now more strict
2. phase 3 completed (with a test)
3. simple optimizer for redundant jumps implemented

- we now use a streaming architecture (run time gain: 11 secs)
- we added some time stamp support

auto-param "size" missing

debug=false

Signature_of has been closed with respect to constructors.

The signature in "retrieve equations" must be extended with the equality if
not already there, otherwise it may hardly find any equation.

some other simplification

ordered_set simplified

exercise ready

exercise ready

almost there

...

First attempts at the third phase.