Bug fixed: nodes were copied.

interpret non ambiguous symbols ASAP

...

allows auto before eq is defined

...

Fixes unexpected behaviour of ncut when multiple goals are selected.

Experimental enhancements to the ndestruct tactic. By using the syntax

ndestruct (e1 ... em) skip (H1 ... Hn)

the user can tell the tactic that
- only equations e1 ... em should be considered
- rewriting should happen only in hypotheses H1 ... Hn and in the goal

both "(e1 ... em)" and "skip (H1 ... Hn)" are optional parameters.

Some experiments on a co-inductive Heityng algebra.

...

some work on \exists

eq -> eq0 renaming

useless box removed

fixed precedence so that no () are needed around variable assignement

do not apply hints if metaclosed

avoid assert false, just fail generating the coercion

...

...

...

...

new icons for the lambda-delta web site

completed lemma 17

...

re 16.4 almost done

big mess of notation

more notation

moved formal_topology into library"

some notation for map_arrows2

...

Some important proofs/definitions were (and are still) commented out and
do not compile.

Added the notion of functor1 to state the main theorem.

Proof simplified.

Proof simplified (??).

...

...

...

...

....

...

notation made half decent

better notation for oalgebra

....

off by one fixed

Fix for inversion principles of types with a single constructor.

Fixed a bug in the undebruijnate function which caused the refiner to produce
a wrong object when refining mutually recursive functions (the references to
recursive calls would contain the wrong index to the recursive argument).

some stuff on re

unify left args of inductive types with left argus of constructors. this allows
to put ? in every left arg of every constructor of an inductive type.

Library support files for John Major equality and Russell.

Experimental support for Russell (coercions moving inside lambda & pattern
matching etc.) added to the refiner.

minimization.ma

little workaround for multiple screens, gdk support not bound by lablgtk2

new intro:
- #; -- introduces into the context every possible assumption giving
        to it an unusable name
- #h1 .. h2; -- multi intros
- intros; -- macro che espande a #h1...hn.

trace generation with "// by _;"

notation

remarks and applyS

Bug fixed: nstatus => status (to undo the changes).

Worring warnings commented out.

...

Fixing naming scheme for composite coercions.

assert false could happen

Bug fixed:

 During unification of E1 with E2, E1 and E2 where not always reduced.
 In particular, reduction was not performed in the cases:
   LetIn vs LetIn, Match vs Match
 and maybe also in some cases Appl Meta vs Appl Meta (who knows?)

coinduction is between us

First tests.

* Fixed a couple of glitches in ndestruct
  - blob equations were not always handled properly
  - tactic used to fail due to not optimal behaviour of the refiner
* Added (experimental) support for JM equality to ndestruct

Regular expressions.

new dependences

From: fguidi <fguidi@c2b2084f-9a08-0410-b176-e24b037a169a>

Elimination of recursive inductive types leads to looping.
ELimnation of singleton types gives problems with negation.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

alpha_eq instead of pervasives.compare

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

bool_ext on 'o' not on 'Prop' (they are convertible, but discrimination
trees do not compare up to conversion)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Formal points.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Some dualization clean-up.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

fixed makefile

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

auto destructs while introducing in the context

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

print nobjects (hack with Obj.magic)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

catch the right exception, avoid uncaught Subst_not_found

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

same heads different arity -> INCOMPARABLE

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

some fixes to THF parser

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

fixed support file for TPTP

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

the edges must be quoted as well (not only the nodes)

From: fguidi <fguidi@c2b2084f-9a08-0410-b176-e24b037a169a>

apply_subst_context on statuses

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

support axioms

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

thf problems list for tptp 4.0.1

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

fixed compiltion order of lexer/parser

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

New code (unbranched) to compute all keys by all possible ways of reducing the term.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

New sets of.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

THF parser received some care

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

Fixing indexing (commit parziale di Claudio?)

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

THF parser for TPTP

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

Not is now inductive.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Use the inversion!

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Bug fixed: the current equation is not always the last hyp.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

- inversion principles are now generated also for co-inductive types
- we use uniformly the cases_tac/elim_tac in the inversion principle

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

More debugging info from print_tac.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Implicit and UserInput were printed incorrectly.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

ninversion

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

removed boh

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

Added test file for inversion in ng matita.

From: ricciott <ricciott@c2b2084f-9a08-0410-b176-e24b037a169a>

Tracing mechanism for auto. Interface changed to solve an ambiguity between
an ampty trace and a missing trace.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>