Avoid killing the main gui thread.

Delift used to produce not well typed substitutions. In turn, this
led to tactics that were not failing immediately, but only at Qed.

Fixed by adding the appropriate check to the delift function.

Note:
 - pass the metavariable number (-1) to avoid the check when you know what
   you are doing (e.g. when delift is just used to restrict a term or to
   replace a term with a convertible one). This used to be 0 (not -1).
 - in some cases (algebraic universes and implicits used to stop chains of
   metavariables) the check is relaxed
 - to make the CerCo script pass (in very "reasonable" and "frequent" cases),
   the algorithm needs to solve the following unification problem:
     S (?[n]) == ?[(S n)]
   Our algorithm used to delift S(?[n]) w.r.t. (S n), yielding x |- ? := x.
   By chance, this was the right solution since S (?[n]) becomes (S n) and
   also ?[(S n)] becomes (S n). However, the two solutions were both added
   to the subst (first bug) and they could even be different (second bug).
   We fix this by checking that they are not different.
   However, at the moment, the solution still occurs twice in the subst....

CC2FO_K_cube: soundness of the K interpretation stated

Comment is now up-to-date.

Matita Web: moved the javascript in a separate file. Bugfixes.

subst.ma: some additions
convertibility.ma: non "conv" refers to the correct predicate
CC2FO_K.ma: CC to Fomega: first interpretation: substitution lemma

Print backtrace of exceptions when OCAMLRUNPARAM=b is setted.

assert false removed

Partial implementation of "go to cursor" action.

auto does not work here :(

basics: some additions
lambda: some additions + split of lift and subst

Better indentation.

Partially working table layout of matita web (only on some browsers).

Debugging code to understand cases where the output notation is not
applied, is applied badly or it raises an assert failure.

Usually the problem is given by optional parts of the term. For instance,
in output all typing information is present and it _must_ be matched.

Name generator for Russell greatly improved.
But maybe we need a longer term solution.

Improved rendering of sequents in matitaweb, including handling of multiple
goals.

Serious bug fixed:
 - in order to look for coercions to sort and funclass, we passed
   types containing implicits and a flag to avoid unification
 - totally avoiding unification, it happened
    1) that we diverged:
       t : A :> B ==> inject t : Sigma x.A :> B ==> eject (inject t): A :> B
    2) that we called unification on types that contained implicits
       (in some cases)

Prod indexed as Dead, that is equal only to itself, instead of Variable that
is equal to anything

Preliminary version of matitaweb handling multiple goals in the sequent view.

Syntax for coercion nocomposites fixed.

Added "nocomposites" to coercions.

- degree: some improvements and the Deg_append lemma
- lambda_notation: the K interpretation (CC to Fomega mapping)

Quick patch to avoid name collisions when passing coercions under let...ins.

Coercions are now propagated under let...ins.

Fixed box pretty printing.

matitaweb: added retract (undo)

degree.ma: we defined the "degree" of a term, which is meaningful in
the lambda-cube

1) interpretation of matches in patterns implemented
2) missing exception added to matitaExcPp

Added support for hyperlinks in the goal view of the web interface.

...

Removed dead code

- we weakened SAT3
- we simplified the specifications of the Cube

want_indent bug fixed

readded function box_of

Compilation fix

Compilation fix

Simplified rendering.

Simplified rendering

Simplified rendering

rm rendering attrs

Removed mathml and proof rendering.

Simplified rendering

Porting to new reduction.

Added matitadaemon.

cube.ma: some pts specifications of the lambda-cube

Porting to the new pts.

Porting to new parametric TJ.

Dummies are blocked.

New version of TJ parametric in the specification of pts.

we added a property

ground: some arithmetical properties added
lift: some properties proved

interim version (added smallLexer)

Record projections:
no need to synthesize an ast term from a CIC term: just use NotationPt.NCic ;
this also fixes a bug that used to prevent generation of projections when the
types of some fields was associated to a notation (example: natural numbers
expressed using \naturals).

Record projections:
no need to synthesize an ast term from a CIC term: just use NotationPt.NCic ;
this also fixes a bug that used to prevent generation of projections when the
types of some fields was associated to a notation (example: natural numbers
expressed using \naturals).

Partial modifications.

we uncommented R3 and R4 tu be used in lambda-delta

- weight: bugfix + weight-based eliminator axiomatized
- notation: bugfix
- lift: first main property axiomatized

- we added notation for the zetable and thetable items
- the first inversion lemma for lift shows a bug in the destruct tactic :(

convertibility.

generatin lemmas and subject reduction (with a lot of axioms).

progress

error in the conversion rule

notation bug fix

- some bug fixes
- we defined the thinning relation

complete reformalization of lambda-delta in matita (initial commit)
first definitions and one lemma

disambiguation of explicit interprettions with arguments now works
i.e. 'eq x y z

...

we added an nmap from NCic.obj to NotationPt.obj (to be continued)

we removed an extra dot from the "include" syntax

we introduced nterm for NotationPt.term

Patch to avoid equations of the form ? -> T (oriented this way) that
can always be applied to later yield non well typed terms.

Moreover, when T is a Leaf and when the goal contains a Leaf, the equation
above is applied breaking one of the "assert (subst=[])" in the code
(since the Leaf is matched by ?).

we proved that the union of two saturated sets is saturated

Keeping track of locations of disambiguated ids and symbols.
Matitac produces disambiguated files, with hyperlinks for ids and § marks
for symbols.
Matita is able to reparse ids with hypelinks.

Fixes previous wrong commit.

1) Second half of the bug fixing for the "lexical keywords lost" bug.
   I expected the need for re-building the lexer also after the Notation command
   and indeed I have found an example for this in CerCo.
2) Printing of compilation result and times required fixed.

Bug fixed: some Uri was not refreshed. The effect of the bug was that some
file was re-compiled even if already compiled.

Debugging code commented out.

- terms.ma: we included 'is_dummy" and "neutral" (maybe "is_neutral
would be better)
- sn.ma rc_sat.ma: we introduced the axioms for dummy

More verbose in case of errors.

red star

Use jmeq from lib.

Nested calls to matitac are now pretty-printed nicely.
The times printed, however, still include the nested compilation time
(to be fixed).

Reindentation.

the weakening lemma is not needed since it is assumed in the rules of
the type judgement :)

the thinning lemma follows immediately from the substitution lemma ...

- lambda_notation.ma: more notation and bug fixes
- terms.ma: contains the data structure of terms and related functions (not involving substitution).
- ext_lambda.ma: cut off of previous ext.ma, containing the lambda-related objects
- subst.ma, types.ma: we removed notation from here
- types.ma: we added special cases of the weakening and thinning lemmas as axioms

Bug fixed and code refactoring: now both matitac and matita include files
correctly by re-generating ~include_paths in the same way and every time a
file is opened (either by matitaScript or by assert_ng itself).

Use matita/lib as the new standard library in place of matita/nlibrary.

Debugging code removed.

sn_prod

sn_lambda

extensions

Bug "fixed" (i.e avoided).

Bug description:
 - matitac (more precisely, MatitaEngine.assert_ng, hence the "include"
   command) parses files differently from Matita. In particular, it works on
   a camlp5 "Grammar.parsable" lexer, which is a lexer that remembers
   look-ahead tokens.
 - an "include" file can change the list of keywords for the lexer
   (e.g. when defining the "if-then-else" notation). Hence, after an include,
   the lexer to be used must change and thus the corresponding
   "Grammar.parsable" should change too. This was not the case since the
   "Grammar.parsable" was not regenerated to avoid loosing the look-ahead
   tokens

Bug avoidance:
 - we assume that the "include" command is properly terminated. Hence no
   look-ahead is performed. After each "include" command we regenerate
   the lexer to avoid the bug.

Note:
 - why don't we need to do this just after a "notation" command?
   Apparently, this is not required. However, I do not understand why.
   Is this to be better understood in the future?

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.

- more notation and service lemmas
- arity.ma: arities and arity types
- arity_eval.ma: arities and arity types assigned to terms

- some ignores
- new service lemmas

dependences fix

added star.ma (star closure of a relation)

Improvements.

diamond property