the refactoring continues ....

now we take the NUri module from the helm-ng_kernel packeage

the refactoring continues

refactoring: helena sources are now in a dedicated directory

txtLexer: bug fix in parsing the string tokens
library: we now export the "meta" attribute
crgXml: crg exportation factorized and alpha conversion now works
crgBrg: we now mark the abstraction and the reverse translation works
ld.dtd: updated to export crg contents

- we simplified the parser return values
- now the display of parser and lexer debug information is controlled
from the command line (with the options -P and -L)
complete_rg: now the empty binders are not treated especially
top: we isolated a fragment of slow code (process_streaming) to be
investigated. It can be enabled with the -1 command line option)
Makefile: we now create the etc directory when it is missing

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>