]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years agoBug fixed in generalization: the goals opened by lazy parsing of the
Claudio Sacerdoti Coen [Wed, 1 Feb 2006 18:35:29 +0000 (18:35 +0000)]
Bug fixed in generalization: the goals opened by lazy parsing of the
generalization argument were not reported correctly. This fix is not
100% correct, but it will do for now. The best solution would be to
add a new tactic to modify the metasenv and to make the status type
private.

18 years agoAbstract and conclusions.
Claudio Sacerdoti Coen [Wed, 1 Feb 2006 17:57:43 +0000 (17:57 +0000)]
Abstract and conclusions.

18 years agoSnapshot
Andrea Asperti [Wed, 1 Feb 2006 16:56:15 +0000 (16:56 +0000)]
Snapshot

18 years agoSnapshot
Andrea Asperti [Wed, 1 Feb 2006 16:26:04 +0000 (16:26 +0000)]
Snapshot

18 years agoline breaking
Stefano Zacchiroli [Wed, 1 Feb 2006 09:18:14 +0000 (09:18 +0000)]
line breaking

18 years agospell checking
Stefano Zacchiroli [Wed, 1 Feb 2006 09:04:13 +0000 (09:04 +0000)]
spell checking

18 years agoPigeonhole proof restructured.
Claudio Sacerdoti Coen [Tue, 31 Jan 2006 18:23:43 +0000 (18:23 +0000)]
Pigeonhole proof restructured.

18 years agoSome more work on the proof of the pigeonhole principle.
Claudio Sacerdoti Coen [Tue, 31 Jan 2006 18:00:08 +0000 (18:00 +0000)]
Some more work on the proof of the pigeonhole principle.
Really tougher than expected.

18 years agoBug fixed in generalize: a status was generated with an old metasenv.
Claudio Sacerdoti Coen [Tue, 31 Jan 2006 17:56:28 +0000 (17:56 +0000)]
Bug fixed in generalize: a status was generated with an old metasenv.

18 years agoadded fix for marangon
Enrico Tassi [Tue, 31 Jan 2006 16:28:05 +0000 (16:28 +0000)]
added fix for marangon

18 years agouse math mode when referencing terms from a \sequent environment
Stefano Zacchiroli [Tue, 31 Jan 2006 16:07:04 +0000 (16:07 +0000)]
use math mode when referencing terms from a \sequent environment

18 years agocommunity review, solved a couple of TODO
Claudio Sacerdoti Coen [Tue, 31 Jan 2006 15:50:06 +0000 (15:50 +0000)]
community review, solved a couple of TODO

18 years ago/me finished reviewing ...
Stefano Zacchiroli [Tue, 31 Jan 2006 13:29:40 +0000 (13:29 +0000)]
/me finished reviewing ...

18 years ago/me reviewed section 4
Stefano Zacchiroli [Tue, 31 Jan 2006 13:25:54 +0000 (13:25 +0000)]
/me reviewed section 4

18 years agofixed
Andrea Asperti [Tue, 31 Jan 2006 12:33:47 +0000 (12:33 +0000)]
fixed

18 years agofixed ocamldep command line
Andrea Asperti [Tue, 31 Jan 2006 12:32:39 +0000 (12:32 +0000)]
fixed ocamldep command line

18 years ago/me reviewed automation subsection
Stefano Zacchiroli [Tue, 31 Jan 2006 12:19:16 +0000 (12:19 +0000)]
/me reviewed automation subsection

18 years agofix
Enrico Tassi [Tue, 31 Jan 2006 12:14:00 +0000 (12:14 +0000)]
fix

18 years agofixed some depends
Enrico Tassi [Tue, 31 Jan 2006 12:09:46 +0000 (12:09 +0000)]
fixed some depends

18 years agoBug fixed: metasenv used in place of metasenv' during rewriting in an
Claudio Sacerdoti Coen [Tue, 31 Jan 2006 10:59:09 +0000 (10:59 +0000)]
Bug fixed: metasenv used in place of metasenv' during rewriting in an
hypothesis.

18 years ago/me reviewed section 3, here I go ...
Stefano Zacchiroli [Tue, 31 Jan 2006 10:55:09 +0000 (10:55 +0000)]
/me reviewed section 3, here I go ...

18 years agominor fixes to ENGLISH
Enrico Tassi [Tue, 31 Jan 2006 10:51:24 +0000 (10:51 +0000)]
minor fixes to ENGLISH
added CoqArt book

18 years agoAdded a new section on automation
Andrea Asperti [Tue, 31 Jan 2006 10:13:20 +0000 (10:13 +0000)]
Added a new section on automation

18 years agosome makefile work
Enrico Tassi [Tue, 31 Jan 2006 09:57:33 +0000 (09:57 +0000)]
some makefile work

18 years ago/me reviewed up to section 2 (included)
Stefano Zacchiroli [Tue, 31 Jan 2006 09:26:21 +0000 (09:26 +0000)]
/me reviewed up to section 2 (included)

18 years agoA new TODO.
Claudio Sacerdoti Coen [Tue, 31 Jan 2006 09:24:23 +0000 (09:24 +0000)]
A new TODO.

18 years agoSome more progress in the proof of the (ad-hoc ?) pigeonhole principle.
Claudio Sacerdoti Coen [Mon, 30 Jan 2006 18:53:18 +0000 (18:53 +0000)]
Some more progress in the proof of the (ad-hoc ?) pigeonhole principle.

18 years agoadded a couple of todo items
Stefano Zacchiroli [Mon, 30 Jan 2006 17:28:13 +0000 (17:28 +0000)]
added a couple of todo items

18 years agofixed cmi:cm(x)a problem in makefiles
Enrico Tassi [Mon, 30 Jan 2006 17:12:13 +0000 (17:12 +0000)]
fixed cmi:cm(x)a problem in makefiles

18 years agosnapshot ...
Stefano Zacchiroli [Mon, 30 Jan 2006 16:45:56 +0000 (16:45 +0000)]
snapshot ...

18 years agoUn TODO rimosso.
Claudio Sacerdoti Coen [Mon, 30 Jan 2006 16:26:27 +0000 (16:26 +0000)]
Un TODO rimosso.

18 years agoSystem section "completed".
Claudio Sacerdoti Coen [Mon, 30 Jan 2006 16:25:46 +0000 (16:25 +0000)]
System section "completed".

18 years agoRewriting steps using the rewriting principles in the library of Matita are
Claudio Sacerdoti Coen [Mon, 30 Jan 2006 16:14:49 +0000 (16:14 +0000)]
Rewriting steps using the rewriting principles in the library of Matita are
now supported.

18 years ago- use kluwer bibtex style for numbered references
Stefano Zacchiroli [Mon, 30 Jan 2006 15:46:50 +0000 (15:46 +0000)]
- use kluwer bibtex style for numbered references
- do not ignore .bbl any longer

18 years ago- minor corrections in the disambiguation section
Stefano Zacchiroli [Mon, 30 Jan 2006 15:32:19 +0000 (15:32 +0000)]
- minor corrections in the disambiguation section
- better screenshot for the authoring interface

18 years agostructured a proof
Stefano Zacchiroli [Mon, 30 Jan 2006 14:49:16 +0000 (14:49 +0000)]
structured a proof

18 years agocorrect name entry {Sacerdoti Coen} in bibtex
Stefano Zacchiroli [Mon, 30 Jan 2006 14:23:36 +0000 (14:23 +0000)]
correct name entry {Sacerdoti Coen} in bibtex

18 years agoCSC/Occam chain-saw/razor on tinycals and library generation/invalidation.
Enrico Tassi [Mon, 30 Jan 2006 14:13:41 +0000 (14:13 +0000)]
CSC/Occam chain-saw/razor on tinycals and library generation/invalidation.
minor changes on patters terminology.

18 years agouniformed terminology used in the indexing part to that used in the rest of the paper
Stefano Zacchiroli [Mon, 30 Jan 2006 13:44:05 +0000 (13:44 +0000)]
uniformed terminology used in the indexing part to that used in the rest of the paper

18 years ago- recreated cicbrowser related screenshots
Stefano Zacchiroli [Mon, 30 Jan 2006 13:25:40 +0000 (13:25 +0000)]
- recreated cicbrowser related screenshots
- minor corrections (mainly TeX macros) in the indexing part
- described cicBrowser in the library part, moved there screenshots, ...

18 years agoTypos
Andrea Asperti [Mon, 30 Jan 2006 12:58:02 +0000 (12:58 +0000)]
Typos

18 years agoDraft of section Indexing and searching.
Andrea Asperti [Mon, 30 Jan 2006 12:53:52 +0000 (12:53 +0000)]
Draft of section Indexing and searching.

18 years agouniformed disambiguation part
Stefano Zacchiroli [Mon, 30 Jan 2006 11:52:27 +0000 (11:52 +0000)]
uniformed disambiguation part

18 years agoAdded whelp to the repository.
Andrea Asperti [Mon, 30 Jan 2006 10:47:07 +0000 (10:47 +0000)]
Added whelp to the repository.

18 years agofew bits for coq comparison of patterns
Enrico Tassi [Mon, 30 Jan 2006 09:25:36 +0000 (09:25 +0000)]
few bits for coq comparison of patterns

18 years agochosmetic
Enrico Tassi [Sun, 29 Jan 2006 19:54:12 +0000 (19:54 +0000)]
chosmetic

18 years agotidied .tex
Stefano Zacchiroli [Sat, 28 Jan 2006 09:12:35 +0000 (09:12 +0000)]
tidied .tex

18 years agotidied .tex
Stefano Zacchiroli [Sat, 28 Jan 2006 08:51:58 +0000 (08:51 +0000)]
tidied .tex

18 years ago1. The last commit that fixed unification of compound coercions with
Claudio Sacerdoti Coen [Fri, 27 Jan 2006 17:32:35 +0000 (17:32 +0000)]
1. The last commit that fixed unification of compound coercions with
   applied atomic coercions used to introduce too many compound coercions
   at the end. In this commit we fix the problem in a brutal way by
   mergin coercions every time CicMetaSubst.apply_subst is called.
   To be refined later on.
2. Several bug fixed in coercions handling. In particular, a coercion whose
   source or target was a name was given an invalid URI and was not unified
   and applied correctly.
3. New version of the algebraic library. In this version we differentiate
   between pre-structures and structures. This allows a few theorems/lemmas
   to be stated in a more natural way.

18 years agoA few paramodulation/demodulation tests moved from library to tests.
Claudio Sacerdoti Coen [Fri, 27 Jan 2006 16:50:21 +0000 (16:50 +0000)]
A few paramodulation/demodulation tests moved from library to tests.

18 years agoBig bug fixed: attributes of constants were forgot during parsing!
Claudio Sacerdoti Coen [Fri, 27 Jan 2006 16:37:59 +0000 (16:37 +0000)]
Big bug fixed: attributes of constants were forgot during parsing!

18 years agoCambiamenti nella parte sulla disambiguazione.
Claudio Sacerdoti Coen [Fri, 27 Jan 2006 12:03:43 +0000 (12:03 +0000)]
Cambiamenti nella parte sulla disambiguazione.

18 years ago- added some cicbrowser screenshot (to be better placed in the text body)
Stefano Zacchiroli [Fri, 27 Jan 2006 08:33:08 +0000 (08:33 +0000)]
- added some cicbrowser screenshot (to be better placed in the text body)
- added list of tables (and thus ignored .lot files)
- moved graphic files in the pics/ subdir

18 years agouse italic by default
Stefano Zacchiroli [Thu, 26 Jan 2006 17:51:24 +0000 (17:51 +0000)]
use italic by default

18 years agoindentation
Stefano Zacchiroli [Thu, 26 Jan 2006 17:51:06 +0000 (17:51 +0000)]
indentation

18 years agoA failing unification of a coercion vs a term is now tried again after
Claudio Sacerdoti Coen [Thu, 26 Jan 2006 17:50:09 +0000 (17:50 +0000)]
A failing unification of a coercion vs a term is now tried again after
a delta-beta weak head reduction of the coercion. This is necessary to handle
the case (f (g ?)) vs (fg t) where f and g are coercions and fg is the
composite coercion.

As a result the notation in algebra is now nicer and more notation can be
parsed.

18 years agono longer requires old diagrams
Stefano Zacchiroli [Thu, 26 Jan 2006 17:08:40 +0000 (17:08 +0000)]
no longer requires old diagrams

18 years agoremoved libraries old dot
Stefano Zacchiroli [Thu, 26 Jan 2006 17:07:25 +0000 (17:07 +0000)]
removed libraries old dot

18 years agoremoved an old figure
Stefano Zacchiroli [Thu, 26 Jan 2006 17:06:38 +0000 (17:06 +0000)]
removed an old figure

18 years agoremoved old version of the matita paper
Stefano Zacchiroli [Thu, 26 Jan 2006 17:05:44 +0000 (17:05 +0000)]
removed old version of the matita paper

18 years agospell checking
Stefano Zacchiroli [Thu, 26 Jan 2006 17:02:43 +0000 (17:02 +0000)]
spell checking

18 years agoignore .log
Stefano Zacchiroli [Thu, 26 Jan 2006 17:02:36 +0000 (17:02 +0000)]
ignore .log

18 years agosome more fixes
Enrico Tassi [Thu, 26 Jan 2006 16:00:54 +0000 (16:00 +0000)]
some more fixes

18 years agosnapshot
Stefano Zacchiroli [Thu, 26 Jan 2006 14:58:51 +0000 (14:58 +0000)]
snapshot

18 years agoreshaped the "authoring interface" part
Stefano Zacchiroli [Thu, 26 Jan 2006 13:20:37 +0000 (13:20 +0000)]
reshaped the "authoring interface" part

18 years agoadded .dot which generated libraries-cluster.{ps,png}
Stefano Zacchiroli [Thu, 26 Jan 2006 10:52:43 +0000 (10:52 +0000)]
added .dot which generated libraries-cluster.{ps,png}

18 years agoadded klocs sums and heading "0." where missing
Stefano Zacchiroli [Thu, 26 Jan 2006 10:13:48 +0000 (10:13 +0000)]
added klocs sums and heading "0." where missing

18 years ago- added components diagram with KLOCs
Stefano Zacchiroli [Thu, 26 Jan 2006 09:56:55 +0000 (09:56 +0000)]
- added components diagram with KLOCs
- fixed some dangling references

18 years agoadded generation of KLOCs in dot diagrams
Stefano Zacchiroli [Thu, 26 Jan 2006 09:38:01 +0000 (09:38 +0000)]
added generation of KLOCs in dot diagrams

18 years agoNew formulation of finite_enumerable_SemiGroups to allow the \iota notation
Claudio Sacerdoti Coen [Wed, 25 Jan 2006 18:00:05 +0000 (18:00 +0000)]
New formulation of finite_enumerable_SemiGroups to allow the \iota notation
to be invertible. However, this does not work (yet) in practice due to
unification between a coercion and a composite coercion. E.g.
 (composite x) vs (f (g ?1))

18 years agoFirst part of a slightly more interesting proof on finite (and enumerable)
Claudio Sacerdoti Coen [Wed, 25 Jan 2006 17:57:48 +0000 (17:57 +0000)]
First part of a slightly more interesting proof on finite (and enumerable)
groups.

18 years ago6hands-introduction to the last two sections
Claudio Sacerdoti Coen [Wed, 25 Jan 2006 17:48:05 +0000 (17:48 +0000)]
6hands-introduction to the last two sections

18 years agoadded gluing among patterns and semantic selections
Stefano Zacchiroli [Wed, 25 Jan 2006 14:23:39 +0000 (14:23 +0000)]
added gluing among patterns and semantic selections

18 years agoadded entry "on the roles of mathml/latex"
Stefano Zacchiroli [Wed, 25 Jan 2006 14:23:26 +0000 (14:23 +0000)]
added entry "on the roles of mathml/latex"

18 years agobugfix: demodulate_tac is in module Saturation
Andrea Asperti [Wed, 25 Jan 2006 08:25:38 +0000 (08:25 +0000)]
bugfix: demodulate_tac is in module Saturation

18 years agoCode restructuring.
Andrea Asperti [Wed, 25 Jan 2006 08:09:21 +0000 (08:09 +0000)]
Code restructuring.

18 years agoAdded some examples for auto/paramodulation/demodulation.
Andrea Asperti [Wed, 25 Jan 2006 08:06:07 +0000 (08:06 +0000)]
Added some examples for auto/paramodulation/demodulation.

18 years agoadded kluwer latex style manual
Stefano Zacchiroli [Tue, 24 Jan 2006 14:29:47 +0000 (14:29 +0000)]
added kluwer latex style manual

18 years agocentered screenshots
Stefano Zacchiroli [Tue, 24 Jan 2006 14:28:31 +0000 (14:28 +0000)]
centered screenshots

18 years agoadded some screenshots
Stefano Zacchiroli [Tue, 24 Jan 2006 11:08:05 +0000 (11:08 +0000)]
added some screenshots

18 years agoadded undamaged version of the icon
Stefano Zacchiroli [Tue, 24 Jan 2006 10:15:01 +0000 (10:15 +0000)]
added undamaged version of the icon

18 years agoremoved damaged icon
Stefano Zacchiroli [Tue, 24 Jan 2006 10:13:04 +0000 (10:13 +0000)]
removed damaged icon

18 years agoright and left cancellation in groups
Claudio Sacerdoti Coen [Mon, 23 Jan 2006 18:49:40 +0000 (18:49 +0000)]
right and left cancellation in groups

18 years agosection re-ordering
Stefano Zacchiroli [Mon, 23 Jan 2006 14:44:46 +0000 (14:44 +0000)]
section re-ordering

18 years agoCenni alla disambiguazione lazy.
Claudio Sacerdoti Coen [Mon, 23 Jan 2006 14:31:10 +0000 (14:31 +0000)]
Cenni alla disambiguazione lazy.

18 years agoignores .toc
Stefano Zacchiroli [Mon, 23 Jan 2006 14:15:58 +0000 (14:15 +0000)]
ignores .toc

18 years ago- s/decompilation/cleaning/
Stefano Zacchiroli [Mon, 23 Jan 2006 14:14:29 +0000 (14:14 +0000)]
- s/decompilation/cleaning/
- highlighted some (un)interesting points in the (de)compilation part

18 years agoreviewer compilation/decompilation part
Stefano Zacchiroli [Mon, 23 Jan 2006 12:45:55 +0000 (12:45 +0000)]
reviewer compilation/decompilation part

18 years agocompleted disambiguation part
Stefano Zacchiroli [Mon, 23 Jan 2006 12:13:00 +0000 (12:13 +0000)]
completed disambiguation part

18 years agolabels here and there
Stefano Zacchiroli [Mon, 23 Jan 2006 10:44:09 +0000 (10:44 +0000)]
labels here and there

18 years agouniformed (G|g)etter with \GETTER
Enrico Tassi [Mon, 23 Jan 2006 10:12:42 +0000 (10:12 +0000)]
uniformed (G|g)etter with \GETTER

18 years ago- towards completion of the disambiguation section
Stefano Zacchiroli [Mon, 23 Jan 2006 07:54:21 +0000 (07:54 +0000)]
- towards completion of the disambiguation section
- some \MATITA and \COQ here and there

18 years ago- use "sec:libmanagement" as label for compilation/decompilation (it was not
Stefano Zacchiroli [Mon, 23 Jan 2006 07:24:49 +0000 (07:24 +0000)]
- use "sec:libmanagement" as label for compilation/decompilation (it was not
  uniformly used before)
- typos in the disambiguation section

18 years agoadded proof of SN for T+ind
Enrico Tassi [Sun, 22 Jan 2006 20:45:01 +0000 (20:45 +0000)]
added proof of SN for T+ind

18 years agodraft of compilation/decompilatio
Enrico Tassi [Sun, 22 Jan 2006 13:43:15 +0000 (13:43 +0000)]
draft of compilation/decompilatio

18 years agoYet another strategy for let...ins: a let-in is _NEVER_ simplified.
Claudio Sacerdoti Coen [Fri, 20 Jan 2006 17:59:43 +0000 (17:59 +0000)]
Yet another strategy for let...ins: a let-in is _NEVER_ simplified.
The user has to use unfold to zeta-expand it.
(Thus, a let-in is more opaque than a constant in the environment.)

18 years agorestructuring
Andrea Asperti [Fri, 20 Jan 2006 13:15:57 +0000 (13:15 +0000)]
restructuring

18 years agoImproved rendering of conjectures
Andrea Asperti [Fri, 20 Jan 2006 12:47:16 +0000 (12:47 +0000)]
Improved rendering of conjectures

18 years agomore structured and indented version of nat.ma
Stefano Zacchiroli [Fri, 20 Jan 2006 12:20:50 +0000 (12:20 +0000)]
more structured and indented version of nat.ma

18 years agobugfix: when looking for a goal from the continuationals stack handle the case that...
Stefano Zacchiroli [Fri, 20 Jan 2006 12:20:30 +0000 (12:20 +0000)]
bugfix: when looking for a goal from the continuationals stack handle the case that no one is there (i.e. the proof is completed) avoiding run-away exceptions