]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

18 years agobugfix: proper computation of the amount of new node shown upon expand
Stefano Zacchiroli [Thu, 20 Jul 2006 10:46:57 +0000 (10:46 +0000)]
bugfix: proper computation of the amount of new node shown upon expand

18 years agoadded -dot to generate dot files
Enrico Tassi [Thu, 20 Jul 2006 09:30:22 +0000 (09:30 +0000)]
added -dot to generate dot files

18 years ago- added to the cicBrowser support for displaying recursive direct/inverse
Stefano Zacchiroli [Wed, 19 Jul 2006 17:34:50 +0000 (17:34 +0000)]
- added to the cicBrowser support for displaying recursive direct/inverse
  dependencies of a given object. To integrate this with cicBrowser's history
  also added a new URI scheme: metadata:/deps/(forward|backward)/URI, where URI
  is the object URI without the trailing "cic:"
- removed automatic stripping of #xpointer(...) from URIs of inductive types

18 years agoNew module to extract from the Db direct and inverse dependencies starting from
Stefano Zacchiroli [Wed, 19 Jul 2006 17:32:43 +0000 (17:32 +0000)]
New module to extract from the Db direct and inverse dependencies starting from
a given URI. Both single step and recursive (in graph form) dependencies are
supported.

18 years agoexported position_prefix (so that it can be looked up from elsewhere)
Stefano Zacchiroli [Wed, 19 Jul 2006 17:31:20 +0000 (17:31 +0000)]
exported position_prefix (so that it can be looked up from elsewhere)

18 years agouse double quotes around escaped URIs, single quotes fail when the URI contains
Stefano Zacchiroli [Wed, 19 Jul 2006 17:30:32 +0000 (17:30 +0000)]
use double quotes around escaped URIs, single quotes fail when the URI contains
a '\'' character

18 years ago- enable header to output graphs attributes and graph-wide node and edge
Stefano Zacchiroli [Wed, 19 Jul 2006 17:29:44 +0000 (17:29 +0000)]
- enable header to output graphs attributes and graph-wide node and edge
  attributes
- quote nodes only when needed

18 years ago- pipe graphviz markup to tred before generating png/map output to get rid of
Stefano Zacchiroli [Wed, 19 Jul 2006 17:28:20 +0000 (17:28 +0000)]
- pipe graphviz markup to tred before generating png/map output to get rid of
  transitive dependencies
- added method center_on_href to clamp viewport so that a given node is visible
  (actually it is not a real "center"ing ...)

18 years agoBug fixed in rewrite in multiple hypothesis and/or conclusion: a lifting was
Claudio Sacerdoti Coen [Wed, 19 Jul 2006 16:29:06 +0000 (16:29 +0000)]
Bug fixed in rewrite in multiple hypothesis and/or conclusion: a lifting was
missing, as usual :-)

18 years ago- added sql statements for querying forward and backward dependencies
Stefano Zacchiroli [Wed, 19 Jul 2006 15:28:24 +0000 (15:28 +0000)]
- added sql statements for querying forward and backward dependencies
- escaped uri which get embedded in sql statements

18 years agoSubmitted a test for inferencing of dependent types.
Claudio Sacerdoti Coen [Wed, 19 Jul 2006 15:11:14 +0000 (15:11 +0000)]
Submitted a test for inferencing of dependent types.

18 years agoadded sets of uri pairs (useful for edges between uris)
Stefano Zacchiroli [Wed, 19 Jul 2006 10:43:43 +0000 (10:43 +0000)]
added sets of uri pairs (useful for edges between uris)
currently commented since not used ...

18 years agoCtr-C now cleans up (with a nice warning :-)
Claudio Sacerdoti Coen [Wed, 19 Jul 2006 10:04:02 +0000 (10:04 +0000)]
Ctr-C now cleans up (with a nice warning :-)

18 years agois_empty_listing fixed: the ls method normalizes away the .gz suffix
Claudio Sacerdoti Coen [Wed, 19 Jul 2006 09:54:03 +0000 (09:54 +0000)]
is_empty_listing fixed: the ls method normalizes away the .gz suffix

18 years agoSerious bug fixed in simplify: sometimes terms wwere not closed because of
Claudio Sacerdoti Coen [Wed, 19 Jul 2006 09:31:33 +0000 (09:31 +0000)]
Serious bug fixed in simplify: sometimes terms wwere not closed because of
the use of the wrong replace function (that did not perform the required lifting).

18 years agobaseuri for group.ma fixed
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 14:33:50 +0000 (14:33 +0000)]
baseuri for group.ma fixed

18 years agohead_beta_reduce can now optionally perform delta reduction too
Claudio Sacerdoti Coen [Tue, 18 Jul 2006 14:30:57 +0000 (14:30 +0000)]
head_beta_reduce can now optionally perform delta reduction too