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)

Too flexible terms are pruned.

commit by user utente1

commit by user andrea

Matitaweb: fixes compilation errors and minor graphical problems.

Matitaweb:
1) Adds a feature to enrich automation statements with their trace (after
   successful execution)
2) Introduces a different syntax (/... trace lemma1, lemma2 .../) for
   system-generated traces (as opposed to user-provided)
3) Graphical update hiding system-generated traces (they are provided as
   a tooltip for inspection, when hovering with the mouse pointer on the
   tactic)
4) Fixes a bug in the computation of the cursor position in the script.

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

Removed some dead code.

New management of justifications.
Justifications do not contain neither facts nor local hypothesis,
hence they must be computed by auto.

commit by user andrea

- file names update

- lib: one lemma about equality was missing
- lambda_delta: one inversion lemma closed

- two discrimination lemmas
- some decidability axioms (proof postponed)

- contex-free normal forms started
- final definition for context-sensitive reduction on local environments
- some refactoring

1. we compare the expected branching with the actual one and
   prune the candidate when the latter is larger. The optimization
   is meant to rule out stange applications of flexible terms,
   such as the application of eq_f that always succeeds.
2. At top level, we index local equalitites for paramodulation for
   each cluster (i.e. we assume metas in a same cluster shares the
   same context *)

At top level, we reindex the local equations for each cluster
(i.e. we assume each cluster shares a same context).

trans_eq and sym_eq indexing restored. Apparently they are useful for several(?)
theorems in CerCo (file positive.ma).

Matitaweb: Added jquery.js (also used in some of the previous releases).

Matitaweb:
1) Added button to strip interpretations from the source
2) Fixed some UI bugs

The proof of append_cons used transitive_eq, not indexed.
If other cases will present we shall reindex it.

Disabled printings.

--Tre the expected branching with the actual one and
       prune the candidate when the latter is larger. The optimization
              is meant to rule out stange applications of flexible terms,
                     such as the application of eq_f that always succeeds.
                            There is some gain but less than expected

                            :his line, and those below, will be ignored--

M    ng_tactics/nnAuto.ml

commit by user andrea

Matitaweb: added layout.js (currently manages resizing of UI).

New management of resulting subst in deep_eq: used to be malformed.

-applicative_case has been rewritten and simplified;
 the strategy should be clear, now.
- if we have an unkown ?n goal we instantiate it with I:True:Prop.
  Due to the topological ordering of goals, ?n should not appear
  in any other open goal, so its instantiation can be arbitrary.
- paramodulation is has only an implicit knowledge of the symmetry
  of equality, hence it is in trouble to prove (a=b) = (b=a).
  A try_sym tactic has been added to smart application to cover this
  case.

Some qed-

some qed-

New management of the resulting substitution in deep eq.
We reduced several time the goal vs the active table, possibly
resulting in a clash of names generating cyclic substitutions.

-pplicative_case has been rewritten and simplified;
  the strategy should be clear, now.
  - if we have an unkown ?n goal we instantiate it with I:True:Prop.
    Due to the topological ordering of goals, ?n should not appear
      in any other open goal, so its instantiation can be arbitrary.
      - paramodulation is has only an implicit knowledge of the symmetry
        of equality, hence it is in trouble to prove (a=b) = (b=a).
          A try_sym tactic has been added to smart application to cover this
            case.-This line, and those below, will be ignored--

M    nnAuto.ml

Matitaweb: Fixed a bug in matitaweb.js concerning disambiguation and escaping.
Added pretty-printing of unhandled NTacStatus.Error exceptions.

refactoring ...

-- some renaming in basic_2

old pr2_subst1 (Basic-1) closed!

Matitaweb: first attempt at web UI for disambiguation.
Also includes a rather radical change in the way the graphical layout is
handled.

Now it should compile :-)

Optimization. Check removed.

Disabled debug.

1. ported to camlp5
2. added a boolean to qed to governe indexing
   the syntax for disabling indexing is "qed-"

typos

We order alternatives according to the number of subgoals they open.

QED takes a boolean parameter governing indexing.
Syntax to avoid indexing is qed-

Alternatives are ordered according to the number of subgoals
they generate.

JMeq lifted to work on Type[1].

Removed some unneeded normalizations from the generation of discrimination
principles (they had a bad effect on performance).

Matitaweb: added preliminary support for interactive disambiguation.
Ambiguous expressions are reported to the client and highlighted.
The possible interpretations are shown in stderr.

Matitaweb: added a function MatitaAuthentication.get_users returning
the list of the registered users.

- the relocation properties of cpr are closed!
- the support for global references is started ...
- some refactoring.