]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years agoapply now uses both menv and subst to decide the fresh meta number
Enrico Tassi [Thu, 21 Sep 2006 13:24:39 +0000 (13:24 +0000)]
apply now uses both menv and subst to decide the fresh meta number

18 years ago"21" -> "Implicit found"
Enrico Tassi [Thu, 21 Sep 2006 13:22:38 +0000 (13:22 +0000)]
"21" -> "Implicit found"

18 years agoadded displaying of the dep graph of a development, click action still missing
Stefano Zacchiroli [Thu, 21 Sep 2006 09:29:14 +0000 (09:29 +0000)]
added displaying of the dep graph of a development, click action still missing

18 years agoadded generation of the .dot version of development dependencies
Stefano Zacchiroli [Thu, 21 Sep 2006 08:54:08 +0000 (08:54 +0000)]
added generation of the .dot version of development dependencies

18 years agoInjection now clears all intermediate results introduced.
Claudio Sacerdoti Coen [Wed, 20 Sep 2006 16:47:13 +0000 (16:47 +0000)]
Injection now clears all intermediate results introduced.
Injection code reindented.
Baseuri in injection.ma fixed.

18 years ago1. bug fixed: injection now performs recursion lifting correctly
Claudio Sacerdoti Coen [Wed, 20 Sep 2006 16:21:53 +0000 (16:21 +0000)]
1. bug fixed: injection now performs recursion lifting correctly
2. bug introduced: injections now behaves as id_tac when it has nothing to do

18 years agoAdded new target linkonly to link matita without re-compiling anything.
Claudio Sacerdoti Coen [Wed, 20 Sep 2006 14:37:19 +0000 (14:37 +0000)]
Added new target linkonly to link matita without re-compiling anything.
Useful for rapid debugging in bytecode.

18 years agolast problem elegantly resolved!
Ferruccio Guidi [Mon, 18 Sep 2006 14:28:30 +0000 (14:28 +0000)]
last problem elegantly resolved!

18 years agoremoved old .cvsignore files
Stefano Zacchiroli [Sun, 17 Sep 2006 14:22:05 +0000 (14:22 +0000)]
removed old .cvsignore files
ready for 3.09.3 and ocaml.mk

18 years agoready for 3.09.3 and ocaml.mk
Stefano Zacchiroli [Sun, 17 Sep 2006 13:39:58 +0000 (13:39 +0000)]
ready for 3.09.3 and ocaml.mk

18 years agobinNMU safe setting of debian/*
Stefano Zacchiroli [Sun, 17 Sep 2006 13:20:29 +0000 (13:20 +0000)]
binNMU safe setting of debian/*
ready for 3.09.3 and ocaml.mk

18 years agoYet another refinement error localized.
Claudio Sacerdoti Coen [Fri, 15 Sep 2006 21:35:36 +0000 (21:35 +0000)]
Yet another refinement error localized.
Enrico should really learn to localize his own exceptions :-)

18 years agoDebugging code deactivated.
Claudio Sacerdoti Coen [Fri, 15 Sep 2006 20:53:55 +0000 (20:53 +0000)]
Debugging code deactivated.

18 years agouseless files removed
Ferruccio Guidi [Fri, 15 Sep 2006 14:14:17 +0000 (14:14 +0000)]
useless files removed

18 years agoexportation completed!!
Ferruccio Guidi [Fri, 15 Sep 2006 12:43:52 +0000 (12:43 +0000)]
exportation completed!!

18 years agoremoved useless file in source package
Stefano Zacchiroli [Thu, 14 Sep 2006 22:33:48 +0000 (22:33 +0000)]
removed useless file in source package

18 years agonew release, binNMU safe
Stefano Zacchiroli [Thu, 14 Sep 2006 22:33:05 +0000 (22:33 +0000)]
new release, binNMU safe

18 years agook up to pc1
Ferruccio Guidi [Thu, 14 Sep 2006 17:53:17 +0000 (17:53 +0000)]
ok up to pc1

18 years ago1. Stricter controls implemented in injection.
Claudio Sacerdoti Coen [Thu, 14 Sep 2006 13:55:57 +0000 (13:55 +0000)]
1. Stricter controls implemented in injection.
2. tests/injection.ma now contains a description of why the tactic sometimes
   fail and there is nothing really cute we can do with it. It also hints to
   an alternative solution implemented in Coq.

18 years agoBug fixed in injection: lifting was not performed correctly, but it worked
Claudio Sacerdoti Coen [Thu, 14 Sep 2006 12:38:12 +0000 (12:38 +0000)]
Bug fixed in injection: lifting was not performed correctly, but it worked
most of the time :-)

18 years ago1. added a test for injection
Claudio Sacerdoti Coen [Thu, 14 Sep 2006 11:58:21 +0000 (11:58 +0000)]
1. added a test for injection
2. injection now works also on inductive types with left parameters

As the test shows, there are still bugs even in the case of an inductive
case with right parameters only.

18 years agoBug fixed in pretty printing in new syntax of MutCases on inductive types
Claudio Sacerdoti Coen [Thu, 14 Sep 2006 10:23:29 +0000 (10:23 +0000)]
Bug fixed in pretty printing in new syntax of MutCases on inductive types
with left parameters.

18 years agoBug fixed in injection: injection can now work on inductive types that have
Claudio Sacerdoti Coen [Wed, 13 Sep 2006 17:22:21 +0000 (17:22 +0000)]
Bug fixed in injection: injection can now work on inductive types that have
right parameters. It is still bugged on inductive types with left parameters.

18 years agook up to pr3
Ferruccio Guidi [Wed, 13 Sep 2006 16:47:31 +0000 (16:47 +0000)]
ok up to pr3

18 years agoremoved contribs from nigtly bench
Enrico Tassi [Wed, 13 Sep 2006 15:37:11 +0000 (15:37 +0000)]
removed contribs from nigtly bench

18 years agosome fixes to the "test notturni"
Enrico Tassi [Wed, 13 Sep 2006 15:31:53 +0000 (15:31 +0000)]
some fixes to the "test notturni"

18 years agoproblems-4 was due to trans_eq expecting an explicit named substitution.
Claudio Sacerdoti Coen [Wed, 13 Sep 2006 15:22:24 +0000 (15:22 +0000)]
problems-4 was due to trans_eq expecting an explicit named substitution.

18 years ago- ok pr0 pr1 pr2
Ferruccio Guidi [Wed, 13 Sep 2006 15:13:47 +0000 (15:13 +0000)]
- ok pr0 pr1 pr2
- added one problem (like problems-4)

18 years ago1. Some warnings about unused warning fixed (hopefully well)
Claudio Sacerdoti Coen [Wed, 13 Sep 2006 14:08:57 +0000 (14:08 +0000)]
1. Some warnings about unused warning fixed (hopefully well)
2. We now try to print the MutCase in the new syntax.
   This fails silently when the type of the constructor is not a spine of Prods
   ended by something not convertible to another Prod. It also fails providing
   reasonable information when one pattern has not enough Lambdas.

18 years agoBug fixed in injection: a missing lift bugged the tactic when the constructor
Claudio Sacerdoti Coen [Wed, 13 Sep 2006 12:53:01 +0000 (12:53 +0000)]
Bug fixed in injection: a missing lift bugged the tactic when the constructor
had more than one argument.
The tactic is still bugged when the inductive type has either right or left
parameters!

18 years agoPossible bug fixed (similar to the previous one, but in another similar function).
Claudio Sacerdoti Coen [Tue, 12 Sep 2006 17:52:57 +0000 (17:52 +0000)]
Possible bug fixed (similar to the previous one, but in another similar function).

18 years agoBug fixed in the guarded_by_descructors function: in some cases the context
Claudio Sacerdoti Coen [Tue, 12 Sep 2006 16:10:22 +0000 (16:10 +0000)]
Bug fixed in the guarded_by_descructors function: in some cases the context
was missing the left arguments! This is the first bug found in the kernel
after quite a long time.

18 years agoBug fixed in the guarded_by_descructors function: in some cases the context
Claudio Sacerdoti Coen [Tue, 12 Sep 2006 15:57:44 +0000 (15:57 +0000)]
Bug fixed in the guarded_by_descructors function: in some cases the context
was missing the left arguments! This is the first bug found in the kernel
after quite a long time.

18 years agoFoo is the problematic elimination principle.
Claudio Sacerdoti Coen [Tue, 12 Sep 2006 13:19:19 +0000 (13:19 +0000)]
Foo is the problematic elimination principle.

18 years agoready for the upload
Stefano Zacchiroli [Mon, 11 Sep 2006 11:28:12 +0000 (11:28 +0000)]
ready for the upload

18 years agoadded me as an author, better formatting of debian/copyright
Stefano Zacchiroli [Mon, 11 Sep 2006 11:27:25 +0000 (11:27 +0000)]
added me as an author, better formatting of debian/copyright

18 years agorebuilt
Stefano Zacchiroli [Mon, 11 Sep 2006 11:26:19 +0000 (11:26 +0000)]
rebuilt

18 years agocommitted the generated version of configure, so that it gets exported upon svn-build...
Stefano Zacchiroli [Mon, 11 Sep 2006 11:19:20 +0000 (11:19 +0000)]
committed the generated version of configure, so that it gets exported upon svn-buildpackage --svn-export

18 years agouse autotools class so that configure is invoked by cdbs
Stefano Zacchiroli [Mon, 11 Sep 2006 11:18:38 +0000 (11:18 +0000)]
use autotools class so that configure is invoked by cdbs

18 years agobumped version
Stefano Zacchiroli [Mon, 11 Sep 2006 11:17:55 +0000 (11:17 +0000)]
bumped version

18 years agosnapshot: first draft of binNMU safe cdbs packaging
Stefano Zacchiroli [Mon, 11 Sep 2006 11:08:40 +0000 (11:08 +0000)]
snapshot: first draft of binNMU safe cdbs packaging

18 years agoadded detection of native code compilation in "upstream" configure/Makefile (going...
Stefano Zacchiroli [Mon, 11 Sep 2006 11:03:15 +0000 (11:03 +0000)]
added detection of native code compilation in "upstream" configure/Makefile (going to remove it from debian/rules now ...)

18 years agooops: changes should be committed to Makefile.in, not to Makefile
Stefano Zacchiroli [Mon, 11 Sep 2006 10:57:08 +0000 (10:57 +0000)]
oops: changes should be committed to Makefile.in, not to Makefile

18 years agook up to arity assignment
Ferruccio Guidi [Sun, 10 Sep 2006 15:19:54 +0000 (15:19 +0000)]
ok up to arity assignment

18 years agoone problem still remains
Ferruccio Guidi [Sun, 10 Sep 2006 10:26:51 +0000 (10:26 +0000)]
one problem still remains

18 years ago3 problems solved patching the alpha-conversion of coq 7.3.1
Ferruccio Guidi [Sun, 10 Sep 2006 10:25:22 +0000 (10:25 +0000)]
3 problems solved patching the alpha-conversion of coq 7.3.1

18 years agoBug fixed: "by ... we proved ... that is equivalent to ...": the is equivalent
Claudio Sacerdoti Coen [Fri, 8 Sep 2006 15:29:40 +0000 (15:29 +0000)]
Bug fixed: "by ... we proved ... that is equivalent to ...": the is equivalent
to part was not considered because of a stupid typo.

18 years agocontentPp.ml (dead code) removed
Claudio Sacerdoti Coen [Fri, 8 Sep 2006 14:05:58 +0000 (14:05 +0000)]
contentPp.ml (dead code) removed

18 years agoDead code (that produces an ugly rendering) removed.
Claudio Sacerdoti Coen [Fri, 8 Sep 2006 10:16:52 +0000 (10:16 +0000)]
Dead code (that produces an ugly rendering) removed.

18 years agoremoving unnecessary files
Ferruccio Guidi [Fri, 8 Sep 2006 09:42:26 +0000 (09:42 +0000)]
removing unnecessary files

18 years ago- some theorems from levels_defs
Ferruccio Guidi [Fri, 8 Sep 2006 09:41:37 +0000 (09:41 +0000)]
- some theorems from levels_defs
- a new problem

18 years agook up to tau0
Ferruccio Guidi [Thu, 7 Sep 2006 18:01:42 +0000 (18:01 +0000)]
ok up to tau0

18 years agoMissing alias added.
Claudio Sacerdoti Coen [Thu, 7 Sep 2006 15:15:16 +0000 (15:15 +0000)]
Missing alias added.

18 years agoPreamble is now working properly and it does not include unwanted aliases.
Claudio Sacerdoti Coen [Thu, 7 Sep 2006 14:02:05 +0000 (14:02 +0000)]
Preamble is now working properly and it does not include unwanted aliases.

18 years agoerror in preamble.ma
Ferruccio Guidi [Thu, 7 Sep 2006 13:19:25 +0000 (13:19 +0000)]
error in preamble.ma

18 years agosubst0 completed
Ferruccio Guidi [Thu, 7 Sep 2006 12:31:09 +0000 (12:31 +0000)]
subst0 completed

18 years agosome theorems about getl
Ferruccio Guidi [Wed, 6 Sep 2006 16:49:52 +0000 (16:49 +0000)]
some theorems about getl

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