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.

Corrected a bug relative to the application of substs in the "on goal"
case.

Added reverse rewriting principle in Type[0].

Some integrations to the ng library.

Added syntax for ninversion tactic (still experimental).

Constants are indexed using the Reference, not the Uri, so that constructors
are different!

Fixed a bug in the unification, which prevented some reduction steps from being
performed in the case "match vs. match", when the types of the matching term
were not the same. The procedure used to always raise an Uncertain exception,
while in many cases the good choice would be to raise KeepReducing. This caused
the nnormalize tactic to fail with an error in some cases.

-bugfix in the "profile" entry

- pipeline support for generated entities in text mode completed

Minimal example in Z showing a problem in the nnormalize tactic.

- a couple of new entities

- the text model now supports invocations of the entity generator (to
be implemented)
- the XML objects can be exported to a specified directory (via the -x
command line option)

- we completed the text parser fixing the syntactic shortcuts
- we can now parse several files without loosing the status
- some imperative variables refactored

- we added some syntactic sugar in the text parser

- we implemented the hierarchy and sort names declaration in text parser
- we implemented a basic taxonomy for the entities in the text parser
- we fixed the visibility rules in the text-to-crg transformation
- we corrected a bug in the text-to-crg transformation (a continuation was not called)
- we removed the hierarchy parameter from the type checker status
- we created an directory with the examples we can typecheck
- we changed the semantics of the -r command-line option

Open goals fixed (it also returned closed goals).

- we added a parser for lambda-delta textual syntax (file extension .hln)
- we now parse the input files with a straming policy
- we added a Meta attribute for explanatory metalinguistic comments
- brg: missing type casts were not inserted (fixed)

Removed debug printings.

added lazy

Nuova versione di auto.

New proofs.

Wilmer's stuff for destruct.

Added an implicit parameter to branch_tac to allow branching on a
single goal.

More theorems

Minor fixings.

The height of fixpoint applications was not computed correctly.

 cerco documentation

minimal sequent height set to 1

some experiment filtering with height

addenda

Added a count_occurrences function.

Bug fixing.

Removed debug printings.

Some changes towards integration of setoid-rewriting.

 freescale porting

 freescale porting

 freescale porting

...

Added count_occurrences.
Type of does_not_occur corrected.

Bug fixed: goto_top used to reset the status to the first one and then
reset_buffer (re-implemented yesterday) used to do the time travel
again. Fixed by getting rid of goto_top.

Note: the old implementation was slightly more efficient since the
initial notation of Matita was not re-loaded every time you go back to
top. In practice, this does not seem to matter.

 freescale porting

 freescale porting

...

End of curryfication of binary_morphisms.

Curryfication of binary_morphisms.

Curryfication of binary setoids.

Curryfication of binary morphisms.

Work in Progress: Who needs binary_morphisms? Curryfication is your friend.

But...

 1) the hints are uglier
 2) you really need to apply mk_binary_morphism to prove a curryfied binary
    morphism if you want to remain sane...

Note: with non uniform coercions everywhere we should be able to finally get
a beautiful script. Yet to be done.

Disabled debug prints in ndestruct tactic.

Debug code commented out.

Parts of the status were not re-initialized correctly during a reset.
Fixed (and bugs avoided).

Bad variable name fixed.

Bug fixed: projection redexes obtained reducing other projection redexes were
not reduced.

New version using Streicher's K axiom. Should be faster and also work with
indexed inductive types.

Added Streicher's K axiom.

Fixed a bug with indexed inductive types which sometimes prevented the
inversion principles from being defined.

 freescale porting

lists

Booleans

boolean arithmetics

 freescale porting

minus

On the last goal at maxdepth we stop at the first solution.

 freescale porting

 freescale porting

 freescale porting

minus in nat.ma

Nuova gestione della width.

 freescale porting

 freescale porting

le_arith

Unfolded exact letins during proof reconstruction.

Added a parameter no_implicit (default true) to choose between raising
assert false or returning the identity.

 freescale porting

le_arith

 freescale porting

 freescale porting

 freescale porting

 freescale porting

 freescale porting