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>

Good definition found.

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

(Co)Inductively Generated Formal Topologies (not only basic ones)

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

patched the definition of locate, advances in locate_add; still issues..

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

Z.ma updated to reflect changes in the logical Not operator

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

Automation problem

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

More work

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

cosi va (se vi pare).

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

...

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

Conflict(?).

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

Extension of demod to arbtrary predicates (not just equalities).

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

Nice examples for automation (that fails).

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

Simplified proof after pattern fix

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

"Not" is no longer a definition

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

The precedence of ^-1 has changed.

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

Equality has one right parameter and thus it's elimination principle has two
arguments to be protected by the scope, not 1. Why did I put one long ago in
place of 2? Maybe we were working on the old library where rewriting was non
dependent?

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

...

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

Axioms were not indexed.

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

Axioms were not indexed.

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

...

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

Real numbers as co-inductive streams of digits (overlapping refining intervals).

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

Computation of the trace.

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

typo in a proof

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

One more case.

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

Readded eqf_2.

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

symmetric_eq -> sym_eq

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

Re-proved an axiom

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

Commented a few lemmas (copies).

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

Fixed a few bugs

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

"flat" function (subst unfolding)

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

Keeping only lift_aux e subst_aux (renamed to lift and subst).

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

Moved compare in a different file.

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

Downgrading level of infix notations involving \sup.

Porting alla nuova def. di negazione

Nuova versione di not.

Printings removed.

Debugging disabled.

Debugging disabled.

New demodulation tactics (mostly for debugging purposes).
It is called with "nauto demod".

Exporting the demodulation function.

New option "demod" for auto.

Porting the new definition of equality.

Do not index examples (concrete syntax: nremark).

nremark => `Example (not to be indexed)

app of app inside smart application.

dr
brs line, and those below, will be ignored--

M    ng_tactics/.depend.opt

qualche caso del lemma 5.2.11

OCaml's inferred type simplified.

...

Splitted gpts in two files.

Aggiornamento alla negazione.

Nuova definizione della negazione.

Comparison of two applications with a different number of arguments not
implemented yet.

1) intros cleans up the cache (because the context changes) and this means
   that the case of an empty list of under_inspection is possible
2) every time we merge goals we need to remove the currently under inspection
   goal from the list

refreshing of inferred type was missing

...

First version of PTS

New definition of negation

Subst was missing in perforate small (apparently, gty is not
meta-closed).

removed debug from the inteface

In line with the ml.

1. For smart application, we only perforate small terms (terms with sort
Type0). E.g. Not(P(a)) is perforated to Not(P(?)) and not to Not(?) as
before.
2. At maxdepth, we restrict the analysis to facts only in case the goal
is not reducible to a Pi. Example: if Not A = A -> False, Not A is not a
fact, and the previous politics would prune its application.

Small changes for debugging

Fixed a bug in deep_eq: we generated new clauses but neglected the
relocating subst. Caused problems in proof reconstruction.