precedence level of if-then-else fixed

Added elimination principles for destructuring let-ins.

Some integrations from CerCo. In particular:

1) notation for destructuring let-ins for pairs, triples, quadruples, etc.
2) if-then-else is now a notation for pattern matching on booleans

support -axiom to avoind indexing an axiom (since there is no qed)

- we improved and updated the generated web pages

Pairs are now records.

Pros: projections from concrete records are now automatically reduced away.
Cons: the name of the constructor is no longer pair, but mk_Prod.

Parentheses are now needed. I do not know why and when this has changed.

Matitaweb: changes to matitadaemon.ml to make it work with new secure user db.

Matitaweb: added utility for conversion of user dbs from the old to the new
format.

Re-Ported to

- camlp5 version 6.02.2 + patches
- ocaml version 3.11.2-4

If you are still using the old version of OCaml + Camlp5, do not update
these two files.

Matitaweb: secure SHA-256 encryption for passwords.
Includes an utility for converting the user db to the new format.

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

nat library reorganized ....

Generalization to any alphabet. We do not need a finite
alphabet since in any case the chars occurring in the regular
expressions are finite.

- slicing relation for the global environment defined (gdrop)
- two arithmetical lemmas inlined

list.ma moved inside lists.
Minor integrations.

closing more axioms

updating the information on lambda_delta

Maietty suggested to change a paragraph on the devel on the Basic Picture

Maietti suggested to replace a paragraph about the development on the
Basic Picture

Closing some axioms...

\vee notation for boolean or

new files started ...

other addition to the standard library removed

we added a definition and a couple of lemmas

- support for atomic arities and candidates of reducibility started
- integrations to standard library reduced
- some refactoring

Grammar change: let corecs can take no arguments (and they have no recursive
argument).

Fixes a bug that overwrited the index of the recursive occurrence of a CoFix,
causing the resulting term to always use the first corecursive definition
of the same block.

Listb contains some boolean functions over lists.

Matitaweb:
1) Added disambiguation error diagnostics, with web GUI
2) Detached MultiPassDisambiguator (still waiting to purge the code, though)
3) Detached stand alone GUI (i.e. matita and matita.opt)

naive sets (A-> Prop)

More properties of iff

Decidability of equality (draft)

component "reducibility" updated to new syntax!

component "unfold" updated to new syntax ...

component "substitution" updated to new syntax ...

- "grammar" component updated to new syntax ...
- notation for lthin
- bugfix in replace.sh

Ground_2 ported to new syntax ...

bugfix in clearing the replaced variable: a relocation was missing

Destruct: we warn about the substituted variable to remove.
In this way, now we know that this is the wrong variable sometimes
(esp. when the equations are more than one).
A bugfix will follow

- now destruct tries to clear the replaced variables (from wilmer's
patch)
- dependences update

fixed DESTDIR

fixed DESTDIR

Changes to disambiguation:

* bug fixed: when pruning from the disambiguation domain symbols with
  just one interpretation, not all of them were pruned
* improvement: errors due to symbols with no interpretation are now
  immediately detected

Changes to refinement:

* major improvement:
  one error was always raised as an Uncertain; it is now raised as a
  Failure when it is the case (i.e. a term/type is found where a sort is
  expected and the term/type has no flexible head).
  This bug fix exponentially decrease the number of refinements performed
  in the disambiguation of some terms in ASM/Status.ma in CerCo

Basic_2 file names update

Syntax change:  change where what => change what where.

regular expressions

Filtering all equations that cannot be embedded (containing metas in the blob).

Passing the correct subst a metasenv when idexing local equations.

Passing the right subst and metasenv when indexing local equations.

Added a test for paramodulation filtering terms with metas inside the blob,
that is with metas under binders, match & co.

More debugging info

Assert false removed (in line with the variable case).

{pattern} => in pattern;

{pattern} => in pattern;

Typo in comment

hints

coercions

Solves a bug that caused the auto statistics to refer to objects that are not
loaded in the environment, forcing them to be loaded and causing all sorts of
problems.

Added help for discriminator and inverter.

short notation for "coercion"

...

...

minor Makefile fixes for the release

Auto parameters documented for 0.99.1.

No longer used parameters of auto removed.

The macro /by _/ now expands again to something parsable.

/by {}/ ==> /by/

For release 0.99.1.

* Almost ready for release 0.99.1.
* Syntax changed:
 *H => * as H
 -H1 .. HN => -H1 .. -HN
 intros => ##
 pattern: in ... => {...}
* Library ported to the new syntax

support for candidates of reducibility started ...

intros macro fixed

collapse applications with a Match as head while indexing

collapse applications with a Match as head while indexing

Towards 0.95.1.

Towards the 0.95.1 release.

In preparation of 0.95.1 release.

- lambda_delta: context-free weak head normal forms continued ...
-               delift started ...
- nnAuto: we removed an optimization that breaks lambda_delta

Non working parts of the library commented out.

Never ported to new syntax.

inversion replaced by elim (???)

support for weak head normal forms started ...

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

Fixes a bug in NnAuto: printing the statistics triggered loading of
objects from the library into the environment.

commit by user andrea

Matitaweb: Fixed typo which caused the compilation of matitadaemon.ml
to fail.

Matitaweb: goto bottom can now be undone step by step and also reports errors
(basic error reporting as in advance).
Should fix a problem with the status.

non-facts local candidates must be applied too in presence of
a trace

non-facts local candidates must be applied too in presence of
a trace

file names and description update

- we proved that context-free reduction admits no one-step loops

Bug fix in inversion:
1) Dependent inversion only makes sense for JMeq
2) Removed test line fixing is_dependent = true

Assert false is no longer true due to tooflex filtering.

Added dependent inversion (default case for jmeq)