]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years agoBugs fixed:
Enrico Tassi [Wed, 6 Sep 2006 16:19:25 +0000 (16:19 +0000)]
Bugs fixed:
 1. matitamake now correctly creates dependencies of the form "A/f.mo: ..." (it used to create
    useless dependencies of the form "/T/A/f.mo: ...")
 2. matitamake is now more (indeed too much) verbose when matitadep fails

18 years agomatitadep used to raise Not_found on empty files and in some other occasions.
Enrico Tassi [Wed, 6 Sep 2006 16:17:43 +0000 (16:17 +0000)]
matitadep used to raise Not_found on empty files and in some other occasions.
Fixed.

18 years agoremoving unnecessary file
Ferruccio Guidi [Wed, 6 Sep 2006 14:46:15 +0000 (14:46 +0000)]
removing unnecessary file

18 years agodependences fixed
Ferruccio Guidi [Wed, 6 Sep 2006 14:45:44 +0000 (14:45 +0000)]
dependences fixed

18 years agoplist added
Ferruccio Guidi [Wed, 6 Sep 2006 12:24:51 +0000 (12:24 +0000)]
plist added

18 years agoremoving working file
Ferruccio Guidi [Tue, 5 Sep 2006 17:45:10 +0000 (17:45 +0000)]
removing working file

18 years agonew theorems
Ferruccio Guidi [Tue, 5 Sep 2006 17:44:29 +0000 (17:44 +0000)]
new theorems

18 years agofixed coercions. composite can't occur if to funclass
Enrico Tassi [Tue, 5 Sep 2006 15:48:19 +0000 (15:48 +0000)]
fixed coercions. composite can't occur if to funclass

18 years agofixed includes
Enrico Tassi [Tue, 5 Sep 2006 08:59:12 +0000 (08:59 +0000)]
fixed includes

18 years agoother working theorems + iso_trans axiomatized (proof saved in problems)
Ferruccio Guidi [Mon, 4 Sep 2006 19:03:44 +0000 (19:03 +0000)]
other working theorems + iso_trans axiomatized (proof saved in problems)

18 years agoBIG FAT COMMIT REGARDING COERCIONS:
Enrico Tassi [Mon, 4 Sep 2006 15:51:36 +0000 (15:51 +0000)]
BIG FAT COMMIT REGARDING COERCIONS:
- multiple coercions from the same type
- coercions to funclass
- fixed cicPp for letin and pi
- improved coercions ma with a minimal test for funclass
- cheanged XML and Ast to support `Coercion ARITY label
- added syntax:
  coercion URI ARITY
  recordfield :ARITY> type
- added topological sorting module (funcotr) in extlib
- abstracted graphviz to allow non strict and tred graphs
- tentative (not yet properly done) of hiding coercions in content
- fixed a problem in metadata contraints iof there are no constraints
- renamed/moved/commented some functions (eat_prod related) in the refiner
- crossed fingers

18 years agofirs error: iso/props
Ferruccio Guidi [Mon, 4 Sep 2006 15:34:18 +0000 (15:34 +0000)]
firs error: iso/props

18 years agoMore aliases.
Claudio Sacerdoti Coen [Mon, 4 Sep 2006 14:46:00 +0000 (14:46 +0000)]
More aliases.

18 years agono-indent
Enrico Tassi [Mon, 4 Sep 2006 14:22:34 +0000 (14:22 +0000)]
no-indent

18 years agoremoved non XML comment line
Enrico Tassi [Mon, 4 Sep 2006 14:21:30 +0000 (14:21 +0000)]
removed non XML comment line

18 years agothe in clause of the match costruction was wrongly output
Ferruccio Guidi [Mon, 4 Sep 2006 13:43:17 +0000 (13:43 +0000)]
the in clause of the match costruction was wrongly output

18 years agoAliases are now wrote down even during the first pass.
Claudio Sacerdoti Coen [Mon, 4 Sep 2006 13:40:01 +0000 (13:40 +0000)]
Aliases are now wrote down even during the first pass.
The only case they are not written down is that of multiple passes.
This makes the scripts more robusts and faster.
We still need (more and more) one shot aliases.

18 years agomatitac now fails if it tries to insert a new alias
Claudio Sacerdoti Coen [Mon, 4 Sep 2006 13:31:55 +0000 (13:31 +0000)]
matitac now fails if it tries to insert a new alias

18 years agonew organization of the Base and LambdaDelta modules
Ferruccio Guidi [Mon, 4 Sep 2006 13:18:17 +0000 (13:18 +0000)]
new organization of the Base and LambdaDelta modules

18 years agoGeneration of inductive and inversion principles for mutual
Andrea Asperti [Mon, 4 Sep 2006 11:27:49 +0000 (11:27 +0000)]
Generation of inductive and inversion principles for mutual
inductive types (before only single types were allowed).

18 years agoBug fixing. If the inductive types do not occur in t, t is
Andrea Asperti [Mon, 4 Sep 2006 11:21:26 +0000 (11:21 +0000)]
Bug fixing. If the inductive types do not occur in t, t is
strictly positive.

18 years agomoving files
Ferruccio Guidi [Mon, 4 Sep 2006 10:51:47 +0000 (10:51 +0000)]
moving files

18 years agorebuilt
Stefano Zacchiroli [Mon, 4 Sep 2006 10:35:15 +0000 (10:35 +0000)]
rebuilt

18 years agoLambdaDelta.ma and some slices of it that typecheck ok!
Ferruccio Guidi [Sat, 2 Sep 2006 12:53:45 +0000 (12:53 +0000)]
LambdaDelta.ma and some slices of it that typecheck ok!

18 years agonew problem:
Ferruccio Guidi [Fri, 1 Sep 2006 18:48:33 +0000 (18:48 +0000)]
new problem:
generation of LambdaDelta.ma fails because of complex Cases costructions

18 years agoBase.ma now ok!!
Ferruccio Guidi [Fri, 1 Sep 2006 18:42:06 +0000 (18:42 +0000)]
Base.ma now ok!!

18 years ago- semantics of tactic subst allmost fixed
Ferruccio Guidi [Thu, 31 Aug 2006 17:41:07 +0000 (17:41 +0000)]
- semantics of tactic subst allmost fixed
- new tactical progress implemented (not working yet :( )

18 years agofixing the semantics of subst
Ferruccio Guidi [Thu, 31 Aug 2006 08:56:16 +0000 (08:56 +0000)]
fixing the semantics of subst

18 years agoa bit of improvement
Ferruccio Guidi [Wed, 30 Aug 2006 19:45:05 +0000 (19:45 +0000)]
a bit of improvement

18 years agoaliases removed
Ferruccio Guidi [Tue, 29 Aug 2006 18:08:08 +0000 (18:08 +0000)]
aliases removed

18 years agoadded a preamble file with disambiguation information
Ferruccio Guidi [Tue, 29 Aug 2006 17:50:20 +0000 (17:50 +0000)]
added a preamble file with disambiguation information

18 years ago- new tactic subst removes simple non recursive equalities from the context
Ferruccio Guidi [Tue, 29 Aug 2006 13:57:23 +0000 (13:57 +0000)]
- new tactic subst removes simple non recursive equalities from the context
- RELATIONAL updated to use the new tactic

18 years agocic/test.ml moved to binaries/utilities
Claudio Sacerdoti Coen [Tue, 29 Aug 2006 13:46:22 +0000 (13:46 +0000)]
cic/test.ml moved to binaries/utilities

18 years agoDocumentation for let-rec fixed.
Claudio Sacerdoti Coen [Tue, 29 Aug 2006 13:22:03 +0000 (13:22 +0000)]
Documentation for let-rec fixed.

18 years agotest file with some bugs
Ferruccio Guidi [Tue, 29 Aug 2006 11:00:22 +0000 (11:00 +0000)]
test file with some bugs

18 years ago- bumped year
Stefano Zacchiroli [Tue, 29 Aug 2006 10:33:26 +0000 (10:33 +0000)]
- bumped year
- up to date FSF address

18 years ago- Level-1: some problems solved
Ferruccio Guidi [Mon, 28 Aug 2006 18:42:45 +0000 (18:42 +0000)]
- Level-1: some problems solved
- legacy: one alias added

18 years ago- Level-1: some fixes to the extraction procedure
Ferruccio Guidi [Mon, 28 Aug 2006 18:17:18 +0000 (18:17 +0000)]
- Level-1: some fixes to the extraction procedure
- tactics: subst id now works (preliminary)

18 years ago- makefile added
Ferruccio Guidi [Sun, 27 Aug 2006 10:34:09 +0000 (10:34 +0000)]
- makefile added

18 years ago- record constructor alpha-converted
Ferruccio Guidi [Sun, 27 Aug 2006 10:23:53 +0000 (10:23 +0000)]
- record constructor alpha-converted

18 years ago- Level-1: added two problems
Ferruccio Guidi [Sun, 27 Aug 2006 10:17:54 +0000 (10:17 +0000)]
- Level-1: added two problems
- legacy: added some aliases
- CicNotationPp: fixed output syntax of records

18 years ago- Level-1: added some problems
Ferruccio Guidi [Sat, 26 Aug 2006 14:02:17 +0000 (14:02 +0000)]
- Level-1: added some problems
- legacy: some now aliases

18 years ago- changed baseuri
Ferruccio Guidi [Sat, 26 Aug 2006 11:29:30 +0000 (11:29 +0000)]
- changed baseuri

18 years ago- removed () around sorts
Ferruccio Guidi [Sat, 26 Aug 2006 11:19:15 +0000 (11:19 +0000)]
- removed () around sorts

18 years ago- added some aliases
Ferruccio Guidi [Sat, 26 Aug 2006 11:16:56 +0000 (11:16 +0000)]
- added some aliases

18 years agochanged baseuri
Ferruccio Guidi [Sat, 26 Aug 2006 11:12:55 +0000 (11:12 +0000)]
changed baseuri

18 years ago- added problem 2
Ferruccio Guidi [Sat, 26 Aug 2006 11:05:17 +0000 (11:05 +0000)]
- added problem 2
- changed baseuri
- some fixes

18 years ago- Unified : some definitions of unified \lambda\delta
Ferruccio Guidi [Sat, 26 Aug 2006 06:59:13 +0000 (06:59 +0000)]
- Unified    : some definitions of unified \lambda\delta
- level-1    : \lambda\delta exported from Coq (not working)
- RELATIONAL : added some notation
- cicNotation: some patches to the parser and pp to make them match

18 years agotrying to make output notation parsable
Ferruccio Guidi [Fri, 25 Aug 2006 15:07:57 +0000 (15:07 +0000)]
trying to make output notation parsable

18 years agosome properties of NLE
Ferruccio Guidi [Thu, 24 Aug 2006 18:50:34 +0000 (18:50 +0000)]
some properties of NLE

18 years ago- new legature == for \equiv used in the notation for NPlus
Ferruccio Guidi [Thu, 24 Aug 2006 18:42:12 +0000 (18:42 +0000)]
- new legature == for \equiv used in the notation for NPlus
  FIXME: notation precedence not correct w.r.t. \to \land ...
- added notation for NLE
- added a comment to dependenciesParser.ml :p

18 years agonew naming
Ferruccio Guidi [Wed, 23 Aug 2006 08:04:36 +0000 (08:04 +0000)]
new naming

18 years agoremoving old contrib dir
Ferruccio Guidi [Wed, 23 Aug 2006 07:46:11 +0000 (07:46 +0000)]
removing old contrib dir

18 years agochanging the contribution name
Ferruccio Guidi [Wed, 23 Aug 2006 07:44:24 +0000 (07:44 +0000)]
changing the contribution name

18 years agonew naming
Ferruccio Guidi [Wed, 23 Aug 2006 07:24:43 +0000 (07:24 +0000)]
new naming

18 years agoinfo about where to find LablGtkSourceView now
Stefano Zacchiroli [Tue, 22 Aug 2006 13:34:39 +0000 (13:34 +0000)]
info about where to find LablGtkSourceView now

18 years agolablgtksourceview is moving to gna, removing the old stuff available here
Stefano Zacchiroli [Tue, 22 Aug 2006 13:32:17 +0000 (13:32 +0000)]
lablgtksourceview is moving to gna, removing the old stuff available here

18 years ago...
Enrico Tassi [Mon, 21 Aug 2006 08:41:29 +0000 (08:41 +0000)]
...

18 years ago...
Enrico Tassi [Mon, 21 Aug 2006 08:35:45 +0000 (08:35 +0000)]
...

18 years agonew naming
Ferruccio Guidi [Sun, 20 Aug 2006 20:05:44 +0000 (20:05 +0000)]
new naming

18 years agonew definitions
Ferruccio Guidi [Sun, 20 Aug 2006 19:44:22 +0000 (19:44 +0000)]
new definitions

18 years agotouched changelog, ready for a release!
Stefano Zacchiroli [Sun, 20 Aug 2006 16:10:18 +0000 (16:10 +0000)]
touched changelog, ready for a release!

18 years agonew naming
Ferruccio Guidi [Sun, 20 Aug 2006 12:19:55 +0000 (12:19 +0000)]
new naming

18 years agobumped gmetadom dependencies to >= 0.2.4
Stefano Zacchiroli [Sun, 6 Aug 2006 09:43:34 +0000 (09:43 +0000)]
bumped gmetadom dependencies to >= 0.2.4

18 years ago- added a label_of_uri function to easily change node labels
Stefano Zacchiroli [Tue, 1 Aug 2006 09:53:39 +0000 (09:53 +0000)]
- added a label_of_uri function to easily change node labels
- increased font size and use names as node labels (make CSC happy :))

18 years agoMore debugging output on stderr.
Claudio Sacerdoti Coen [Thu, 27 Jul 2006 17:34:52 +0000 (17:34 +0000)]
More debugging output on stderr.

18 years agoAutomation enabled for declarative proofs. Cool.
maiorino [Thu, 27 Jul 2006 16:45:53 +0000 (16:45 +0000)]
Automation enabled for declarative proofs. Cool.

18 years ago"that is equivalent to" and "or equivalently" implemented in most situations.
maiorino [Thu, 27 Jul 2006 16:21:27 +0000 (16:21 +0000)]
"that is equivalent to" and "or equivalently" implemented in most situations.

18 years agoAll the declarative tactics now have a more or less bugged implementation.
maiorino [Thu, 27 Jul 2006 15:52:31 +0000 (15:52 +0000)]
All the declarative tactics now have a more or less bugged implementation.

18 years agoDeclarative tactics for rewriting steps, elimination of the existential
maiorino [Thu, 27 Jul 2006 14:47:57 +0000 (14:47 +0000)]
Declarative tactics for rewriting steps, elimination of the existential
quantifier and elimination of conjunciton implemented.

18 years agoNotation for the existential quantifier moved to core_notation.moo
maiorino [Thu, 27 Jul 2006 14:46:31 +0000 (14:46 +0000)]
Notation for the existential quantifier moved to core_notation.moo

18 years agoNew declarative commands (ast, pretty-printing and parsing only):
maiorino [Thu, 27 Jul 2006 09:32:47 +0000 (09:32 +0000)]
New declarative commands (ast, pretty-printing and parsing only):
  [obtain term] = term by term
  by term we have term (id) and term (id)
  we proceed by induction on term to prove term
  the thesis becomes term
  by induciton hypothesis we know term
  case id [(id:term)]*

18 years agoprint_endline => prerr_endline
Claudio Sacerdoti Coen [Thu, 27 Jul 2006 09:10:08 +0000 (09:10 +0000)]
print_endline => prerr_endline

18 years agoPatch to the unification to make the case (i l) vs (t l) work when i is
Claudio Sacerdoti Coen [Wed, 26 Jul 2006 15:50:54 +0000 (15:50 +0000)]
Patch to the unification to make the case (i l) vs (t l) work when i is
an inductive type and (t l) must be subject to weak head reduction.

18 years agoDebug code commented out.
Claudio Sacerdoti Coen [Wed, 26 Jul 2006 14:39:46 +0000 (14:39 +0000)]
Debug code commented out.

18 years agoElim now performs whd to find the inductive type.
Claudio Sacerdoti Coen [Wed, 26 Jul 2006 14:05:31 +0000 (14:05 +0000)]
Elim now performs whd to find the inductive type.

18 years agoadded tinycals to the proof we frequently use for examples and screenshots
Stefano Zacchiroli [Wed, 26 Jul 2006 09:24:55 +0000 (09:24 +0000)]
added tinycals to the proof we frequently use for examples and screenshots

18 years agoadded test for reordering of goals when using the 1,2,3: tinycal
Stefano Zacchiroli [Wed, 26 Jul 2006 09:17:25 +0000 (09:17 +0000)]
added test for reordering of goals when using the 1,2,3: tinycal

18 years agoorder is important
Enrico Tassi [Wed, 26 Jul 2006 08:35:34 +0000 (08:35 +0000)]
order is important

18 years agoadded definition of f_equal1. I think this file should not be inside the matita library!
Enrico Tassi [Tue, 25 Jul 2006 09:04:25 +0000 (09:04 +0000)]
added definition of f_equal1. I think this file should not be inside the matita library!
once cercions from /\ to eq will be committed the definition should be replaced by two
coercion statement (that will generate the composite)

18 years agoBug fixed: a symbol alias Symb(s,0) now subsumes the case Symb(s,n) for each n.
Andrea Asperti [Mon, 24 Jul 2006 16:36:26 +0000 (16:36 +0000)]
Bug fixed: a symbol alias Symb(s,0) now subsumes the case Symb(s,n) for each n.

18 years agoDisambiguation passes simplified.
Claudio Sacerdoti Coen [Mon, 24 Jul 2006 14:58:55 +0000 (14:58 +0000)]
Disambiguation passes simplified.

18 years agoA compiling version of the library.
Andrea Asperti [Mon, 24 Jul 2006 14:50:33 +0000 (14:50 +0000)]
A compiling version of the library.

18 years agouse the new graphviz pretty printer API
Stefano Zacchiroli [Mon, 24 Jul 2006 14:28:13 +0000 (14:28 +0000)]
use the new graphviz pretty printer API

18 years agoadded missing dependency
Stefano Zacchiroli [Mon, 24 Jul 2006 14:09:40 +0000 (14:09 +0000)]
added missing dependency

18 years agoequality now requires 2 extra parameters
Stefano Zacchiroli [Mon, 24 Jul 2006 14:09:30 +0000 (14:09 +0000)]
equality now requires 2 extra parameters

18 years agoremoved reference to primes1.ma (now removed)
Stefano Zacchiroli [Mon, 24 Jul 2006 14:09:09 +0000 (14:09 +0000)]
removed reference to primes1.ma (now removed)

18 years agoadded timeout parameter to auto paramodulation.
Enrico Tassi [Mon, 24 Jul 2006 10:32:14 +0000 (10:32 +0000)]
added timeout parameter to auto paramodulation.

18 years agomore work on matitaprover (no more XML and buris are created).
Enrico Tassi [Mon, 24 Jul 2006 09:32:54 +0000 (09:32 +0000)]
more work on matitaprover (no more XML and buris are created).
now matita can start on a .p file.

18 years agomore and more tests
Enrico Tassi [Mon, 24 Jul 2006 08:07:07 +0000 (08:07 +0000)]
more and more tests

18 years agomore static libs for matitaprover
Enrico Tassi [Sun, 23 Jul 2006 09:06:33 +0000 (09:06 +0000)]
more static libs for matitaprover

18 years agosee BOO025-1 as an example of failure if (mot p) is commented out.
Enrico Tassi [Sun, 23 Jul 2006 08:36:35 +0000 (08:36 +0000)]
see BOO025-1 as an example of failure if (mot p) is commented out.

18 years agoadded
Enrico Tassi [Sat, 22 Jul 2006 17:17:47 +0000 (17:17 +0000)]
added

18 years agomatitaprover
Enrico Tassi [Sat, 22 Jul 2006 17:14:13 +0000 (17:14 +0000)]
matitaprover

18 years agoeta_fix default to false
Enrico Tassi [Fri, 21 Jul 2006 14:17:20 +0000 (14:17 +0000)]
eta_fix default to false

18 years agoRevert of the previous situation: when an identifier has no universe all the
Claudio Sacerdoti Coen [Thu, 20 Jul 2006 15:17:46 +0000 (15:17 +0000)]
Revert of the previous situation: when an identifier has no universe all the
passes that does not use the library are doomed to fail and the user will
be asked how to instantiate everyn identifier (not withstanding performances).
Now if an identifier has no universe we look for its interpretations in the
library.

18 years agotrans chains even inside letins body
Enrico Tassi [Thu, 20 Jul 2006 15:10:24 +0000 (15:10 +0000)]
trans chains even inside letins body

18 years agoavoid collapsing node that does not need to be, i.e.:
Stefano Zacchiroli [Thu, 20 Jul 2006 15:02:52 +0000 (15:02 +0000)]
avoid collapsing node that does not need to be, i.e.:
- nodes with no outgoing edges
- nodes which have not been expanded before

18 years agoremoved abstractios for dummy metavariables when generating letins body
Enrico Tassi [Thu, 20 Jul 2006 13:11:23 +0000 (13:11 +0000)]
removed abstractios for dummy metavariables when generating letins body

18 years agoreorganization
Enrico Tassi [Thu, 20 Jul 2006 11:22:15 +0000 (11:22 +0000)]
reorganization