Trick: the refiner always subst-expands the outtype, so that the beta-redex
that will be formed will always be reduced by substitution.

Bug fixed in two lines + 5 lines of comment.
During select, the context of the goal is changed and the conclusion
is changed too (too a ?[out_scope]). Then the changed conclusion was
relocated in the changed context, triggering a delift that in turn triggered
the unification case "something vs ?[out_of_scope]"... at the bad time!
Fixed by manually relocating the new conclusion in the new context.
Manually means opening and building again the cic_term data type, which is
ugly and sort of fragile.

assert_tac now takes a list of sequents and also checks that the number of
sequents is the appropriate one.

It is the first example of a high-tactic that works also with the stack.

New debugging tactic nassert:

 nassert H1: t1 ... Hn: tn \vdash T

asserts (using OCaml's assert) that the current goal is equal (using
OCaml equality) to the one given the user. The substitution is fully
expanded just before calling OCaml equality.

Semantic selection back again (but no semantic cut&paste yet).

Match is now rendered as best as possible.

The sequent viewer now considers the context to render the Rels.

- character: we adjusted some "autobatch" parameters
- limits: in classes and subssets we now ensure the compatibility between the
  inhabitance predicate and the equivalence relation

The substitution is now taken in account when printing sequents in the
sequent viewer. Context is not yet taken in account.

added letin, still broken

...

new tactic whd implemented

- change implemented in 4 lines
- select0 runs on hypothesis
- relocate honors conversion (but clearbody is not implemented)

- generalize finished
- relocate implemented in terms of delift

?_OS1 := C[ ?_IN ]
?_IN := m
=======================
?[m;m]  =?=  ?_OS1

used to yield ? := Rel 2 instead of Rel 1, since the first m
was still out of scope when recursion reaches ?_IN

fixed modules order

minor fixes

...

...

+ Chain  NCic.term -> content -> presentation very very roughly implemented
+ The sequent viewer now prints also the neq sequents

Just to make it compile again.

generalized is half-implemented (still broken)

Analizyng the inductive type of the eliminated term and
the sort of the goals are performed by tactics having
a side-effect. This allows to write tactics like elim and cases
as lists of tactics blocked together.

- nrewrite ((very?) rough implementation)

  PATTERNS DO NOT WORK (why?)

- more progress towards generalize, but I am stuck now
- elim completed (up to saturation)

- select_tac honors the hypotheses pattern when required to generalize them
- clear [names]
- initial generalize tac implementation

select honors the substitution

New tactic clear; new syntax # _; to introduce and immediately clear an
hypothesis.

...

tactic cases works! delift clears tags

eta-contraction was made on the wrong term

unification:
 - the case

    (? args) v.s. ?(tag:OUT_SCOPE)

   is considered as a pattern-driven delifting.
 - the case ? args v.s. t is reduced to ?[args] v.s. t
 - eta-contraction reimplemented
 - beta-expand no longer used

delift:
 - handle out/in scope tag

ntactics:
 - elim sets the out_scope tag for 1 entry

better error message

added one exception

- external quantification removed (will be reintroduced when needed)
- preamble added (was missing)

limits: reorganized and attached to nightly tests (cow compiles fully)

snapshot

- Procedural: now we generate the exact tactic (in place of some apply tactics) and we do not perform conversion steps before it (1104 change tactics omitted in the lambda-delta devel)
- new target for the PREDICATIVE-TOPOLOGY devel: now is "limits"

...

New file nTacStatus to:
 1) collect type declarations and utility functions
 2) make cic_term as abstract as possible

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.