New demod function working for arbitary goals.

models ported

Enforcing the disjoint invariant between metasenvs.

Main change: added a parameter to build_equality_proof to discriminate
bewteen forward and backward rewriting steps.

even more polymorphic dualizer

done

...

lebesge works

WIP

many bugs fixed

metasenv passed to get_relevance, Metas that stand for sorts have shift 0 and len 0

WIP

_ in place of unused variables

Implicit annotationas are now printed

seg_u/l were inverted, more work

big lemma done

...

duality done

almost done, just needs to be prforated

....

all done in declarative style

...

...

duality is a joke

...

leave-environment axiom made true

lebesgue completely dualized

we aligned the implementation to the plmms08 paper

...

better pps

- mk_restricted_irl removed, the non-optimized code was the same
- delift fixed in case Meta (used to produce negative shift/irl-len)
- fix-sorts takes into account the swap parameter to implement cumulativity

psubst for metas fixed again

nat model ported to the dualized version, but not itself dualized dedekind-sig-compl missing

... is a command in proof mode, use
\ldots instead

more bug fixed (or introduced)

...

...

...

after a PITA, lebergue is dualized!

...

...

...

some work on duality, still not finisched

...

...

grave notation mistake fixed

more tests

...

...

when a file is opened the cursor is moved to the begin of the file

...

...

tactic language documented;

Acic2Procedural:
 now we accept an optional string argument "info" intended as a comment for the  rendered proof (appears afer qed)
ProceduralOptimizer:
 - we generate some comments for acic2Procedural.ml info (see above)
 - optimize_term is now available
ApplyTransformation:
 we fixed a bug in the procedural rendering of auto proofs:
 the proof term must be optimized before rendering!
 (it is written on the paper about the procedural rendering for PLMMS 2007)

html documentation generation implemented

more doc

...

...

new command eval added

better makefile

...

...

ex for students about induction

...

delifting a Meta with an IRL w.r.t. another IRL completely changed.
the explanation is on my whiteboard, hope someone copies it

some bug fixed

subst_meta was missing

minor simplification + deps fixed

New invariant and data structure to represent environments, transformation
maps and flat environments (2nd compiler pass).

more work

firs step for dualization

...

term refinement almost done, some functions exported from the kernel since they were re-usable

initial refiner ....

Bug fixed in LetIn: the cumulativity test was performed switching the order
of the arguments!

bug in psubst fixed inside local context in Irl form

better error message

ppmetasenv & subst added

NCicReduction.reduce_machine returns a boolean stating if the machine is in normal form

Fixed a performance problem with unif_machines and small_delta_step.
Previously, small_delta_step would occasionally return two machines in
normal form, with a false "are_normal" flag: this in turn caused
unif_machines to perform more steps than necessary. Now the flag returned
by small_delta_step is true iff it could not perform any reduction step;
therefore unif_machines won't try a recursive call on the new machines
(which are equal to the old ones).

slow example

3 nasty bugs fixed:

- mk_restricted_irl has been duplicated
  - mk_restricted_irl generates an irl
  - mk_perforated_irl generates a restricted local context suitable for a new meta

- a wrong optimization in psubst was lifting of a bad amount

- force_does_not_occurr was not delifting rels to hypotheses to be cancelled

...

...

better test

not so nice patch to small_delta_step

when -debug do not catch the exception

- NCicPp.ppterm applies the substitution
- NCicReduction.are_convertible does not take in input the get_relevance
  function any longer, there is a ref set by the typechecker module
- fixes to the convert-machines and small-delta-step logic

the iterator was wrongly processing the application

Final implementation of proof irrelevant conversion, which hadn't
been committed (!)

better debuggin output

error...

...

another divergence case patched

to avoid a case of divergence small_delta_step checks if terms are flexible and
gives 0 as delta

...

we can test the unification algorithm!

...

commented out unfinished code

...