added analyse_indty

New tactic "case1_tac" that make "intro" followed by case of the first
argument.

It is now possible to write things like:

napply t; ## [ #H | *W; #K1 #K2 ]

...

## prefix is now used for tinycals

Example:  napply H; ##[ #H | #K];

New tactic intro. Syntax: "# n".

added tentative elim

1) mk_meta now returns also the index of the created meta
2) added datatypes for new patterns
3) added tactic nchange (using new patterns)
4) changed the type lowtac so that they no longer return the
   lists of open and closed goals, that are always computable
   in the new system
5) added some wrappers for kernel/refinement functions that
   work on statuses and terms labelled with their context
6) new implementation of select that performs subst-expansion.
   in-scope/out-scope used to mark regions selected by the pattern
7) ugly implementation of change based on re-opening of tagged
   subst entries

removed spurious "

tentative subst-sexpand and change

...

more comments

exec and distribute implemented

new apply almost there

...

...

new tactics are almost ready

...

add Homepage field

set package section to "ocaml"

add missing ${misc:Depends}, thanks lintian!

release to unstable

debian/*.in: more abstract substvars

debian/rules: use ocaml.mk as a CDBS "rules" snippet

refresh build-dependencies for the transition

added mactions, the three can now be collapsed to fit the screen

New parameters for applyS: 10 20.

Adapted to new applyS.

Added a property.

More details on the proof.

New algorithm based on in-place modification of the graph.
Conjecture solved in the negative:

(CMM?)+ | (MM?C)+

cCw = Cw
-Cw = MCw
cMw = CMw
-MMw = -w
-MCw = MMCw
iw = w

matitacLib: Gc.compact added after the compilation of mmas
            Now LAMBDA-TYPES compiles in ~ 100m
Makefile: daily test of LAMBDA-TYPES re-enabled

Procedural: id tactics are not counted, ie they are placeholders
LAMBDA-TYPES: bugfix in depend +
              makefile entries for %.ma %.mma %.ma.opt %.mma.opt

bug fix + better obj flavour guessing via inner sorts

the level 1 reconstruction procedure is now in Procedural1
Procedural2 coming soon ....

....

new dependences

unification hints with recursive calls do work!

added margin option to the pp

more examples

unificatiom hints with premises

added some commented debugging instructions :)

unification hints almost ready

notation ++

A version of applyS with bounded iterations of given_clause (10+10).
Not sure it works on the full library.

Removed the context from the metasenv to avoid trivial typing errors (lists
with different lengths).

...

Minor improvements in pretty-printing.

New version: only new nodes are normalized; moreover, reduction stops as soon
as the term becomes shorter.

- fixed hint generation, more hints are generated
- fixpoint refinement added
- Appl [Meta _; ... ] handled correctly, no double Appl or Beta redex is
  generated (both in regular code and interators)

...

New version.

New version.

New version.

New version.

New version.

New version.

New version.

New version.

First version.

Old algorithm moved to old to leave place to the new one.

cicInspect: node count fixed
proceduralTeX: bug fix
LAMBDA-TYPES/Legacy-2/preamble.ma: bug fix
character: updated

uri renaming and new nodes count

some renaming to comply with new naming policy ...

cicInspect: now we can choose not to count the Cic.Implicit constructors
proceduralTypes, proceduralOptimizer: we do not count the Cic.Implict nodes
proceduralTeX: bug fix

ProceduralTeX completed and tested on the terms given as examples in the paper about the procedural reconstruction

...

...

...

New module for TeX rendering of procedural input/output
Used in the papers about the procedural representation

...

...

- Coq/preamble: missing alias added
- nUri: head comment fixed
- Procedural: the cases tactic is now detected and generated
              but does not compile :))
- grafiteAstPp: output syntax of the cases tactic fixed
- grafiteParser: impovement in the code for the elim tactic

some notational experiments

...

...

...

commented some printings

minor changes to make the library compile after wilmers new exists.

Axiomatization of real numbers (work in progress)

errata corrige.

Fixed a problem of lifting.

some work to refine objs

...

b:action are now considered as m:maction and thus are expanded

...

...

a non necessary but morally required change. The matched term in
are_convertible is compared with test_eq_only=true (not really needed since
if it reduces to something it is a constructor an thus an application that already honors the test_eq_only=true check for arguments

some work to speed up the system

case tactic first tries with a simple outtype and then with a more sofisticated one
only if necessary since refine time may be long

...

CicTypeChecker.typecheck now takes an additional parameter:
- trust:bool, set to false only by the proofChecker daemon, while
  the refiner (for example) passes true

Hmmm, going too low.
We need a more abstract proof (see Theorem 5.15, page 157 old book).

...

Towards fullness.

Renaming.

Renaming.

fix convertibility in case of application test_eq_only is =true for
arguments, since we dont know if reduction eventually moves them in
contravariant position

more polishing

...

application arguments are compared with test_eq_only=true