Ferruccio Guidi [Thu, 24 Nov 2011 22:34:36 +0000 (22:34 +0000)]
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
* 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
Wilmer Ricciotti [Fri, 18 Nov 2011 16:04:58 +0000 (16:04 +0000)]
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.
* 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
Wilmer Ricciotti [Tue, 15 Nov 2011 11:38:04 +0000 (11:38 +0000)]
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.
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.
Andrea Asperti [Thu, 3 Nov 2011 12:48:32 +0000 (12:48 +0000)]
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 *)
Andrea Asperti [Wed, 2 Nov 2011 10:23:45 +0000 (10:23 +0000)]
--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
Andrea Asperti [Fri, 28 Oct 2011 10:58:22 +0000 (10:58 +0000)]
-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.
Andrea Asperti [Fri, 28 Oct 2011 08:40:50 +0000 (08:40 +0000)]
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.
Andrea Asperti [Fri, 28 Oct 2011 08:13:03 +0000 (08:13 +0000)]
-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--
projects / helm.git / log