fixed script to use auto depth=4

eliminazione di un passaggio di transitività in ast2astfe
dimostrazione di un assioma in env2flatenv

Calling unification instead of matching when checking for subsumption
might instantiate the goal with variables in table (while they are supposed
to be disjoint).

- A new interesting elimination principle over inductively generated topologies:
  the elimination principle for general topologies hold!
- A proof of Cantor theorem using formal topologies. By Silvio Valentini.

BDD

removed prerr_endline

debug=false

shannon proved

added shannon

added lazy

Environment simplified.

No longer used.

- New dependency for environments on the nesting depth.
- New invariant that tightly binds the list of identifiers in scope with
  the list of mappings in an environment transformation map
- Second pass of the compiler finally complited

Propagation of changes in paramodulation.

Exported a couple of functions.
--Thi sline, and those below, will be ignored--

M    metadataQuery.mli

Added a in_universe function

propagation of changes in other paramodulation files.

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

...