support for abstract candidates of reducibility closed! ...

more files added to Basic_2

Fixes a bug in is_flexible (when checking a meta in subst, we did a recursive
call on its body without applying the local context, resulting in various
assertion failures).

Better error messages.

- one file added to Basic_2

- main lemmas about abstract reducibility candidates closed
- notation updated (and one bug solved)
- Makefile: stats display improved

Inversion principles generation falls back to cases tactic when elim is not
available.

big fixin the structure of Basic_2

more files to Basic_2

- main proof for strong normalization closed! ...
- bug fix in lenv refinement for abstract candidates of reducibility (lsubc)
- lenv refinement for atomic arity assignment defined (lsuba) and relation
with lsubc proved

closure property S4 added to abstract candidates of reducibility ...

the support for candidates of reducibility continues ...

some additionsand refactoring in Basic_2

more file names added to Basic_2

- the development of abstract reducibility candidates continues ...
- some annotations added

Improves the presentation of hypotheses in the goal pane.

Fixes r11788 (partial, thus broken commit).

unpatched version for the new CamplP5

patched version for old CamlP5

Bugfix: NCicUnification.could_reduce now performs whd in the applied fixpoint
case, to prevent the recursive call from raising assert failure.

A complete snapshot for re

more characters shortcuts

Basic_2: restyling and more notation

- notation restyling ...

Basic_2: - we addedsome files
         - we added some notation
 - we updated the table style

lambda_delta: global environments handling: redefined and first results
              rtm: first definitions
lib/arithmetics/nat: a missing lemma added
predefined_virtuals: we added circled numbers, circled letters and
other characters
depend, depend.opt: regenerated

the support for reducibility candidates evolves ,,,,

Complete version

modified definition of memb

reverse

more properties of union

noteq_to_eqnot

notation and dependences bug fix

Basic 2 page update

- support for candidates of reducibility continues ...
- change in the notation of relatiional relocation and local env.
slicing, to allow more usual notation for functional relocation (not
working yet)

Basic_2 update ...

- the definition of the framework for strong normalization continues ...
- functional version of relocation and core substitution implemented
- standard arithmetics library updated

In case paramodulation fails we apply unit equalities.

Splitted DeqSets in their own file. Notation for memb to hide the type.

Hints sui DeqSets

More stuff from CerCo to the standard library.

Some more lemmas from CerCo.

Matitaweb: large commit porting to the new Matita 0.95 syntax.
Integrates some old patches.
Fixes a bug with GotoPos which prevented errors from being shown.

1) Notation for dependent pairs differentiated from that for sigma types.
2) Russell now works directly on mk_Sig/pi1

Dependent pairs (i.e. Sigma types in Type[0]) are back, but are not the default
ones.

1) PSig and Sig merged into a single Sigma type in Prop.
2) One function in list.ma that required the Sigma type in Type has been
   removed.

inject/eject replaced by mk_Sig/pi1.

1) New file russell with the coercions to activate Russell-style proving.
2) More stuff on lists integrated from CerCo library

Chapter 5 = re.ma ; chapter 6 = moves.ma

New chapter 4

Matitaweb: clicking buttons disables the GUI to prevent another operation from
being issued before the first one has completed.

Splitted re into lang.ma nd re.ma

Sig in Prop

More stuff integrated from CerCo on sigma types (that are now a record)
and option.

axiom-

pair => mk_Prod (one more was left in notation)

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