...

...

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

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