]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years agofixed metaconvertibility that was completely wrong.
Enrico Tassi [Fri, 29 Sep 2006 17:07:53 +0000 (17:07 +0000)]
fixed metaconvertibility that was completely wrong.
is_identity and is_weak_identity fixed accordingly

18 years agoremoved bad guard that was always false (assert false in the line above)
Enrico Tassi [Fri, 29 Sep 2006 17:07:06 +0000 (17:07 +0000)]
removed bad guard that was always false (assert false in the line above)

18 years agofixed (dasabled paramod)
Enrico Tassi [Fri, 29 Sep 2006 14:49:31 +0000 (14:49 +0000)]
fixed (dasabled paramod)

18 years agorenamed inference in founif that is more appropriate
Enrico Tassi [Fri, 29 Sep 2006 14:41:27 +0000 (14:41 +0000)]
renamed inference in founif that is more appropriate

18 years agois_identity -> is_weak_identity
Enrico Tassi [Fri, 29 Sep 2006 14:27:20 +0000 (14:27 +0000)]
is_identity -> is_weak_identity

18 years agohack to make the Pp work (sometimes)
Enrico Tassi [Fri, 29 Sep 2006 14:22:25 +0000 (14:22 +0000)]
hack to make the Pp work (sometimes)

18 years agonew version of auto that is able to prove the irrationality of sqrt(2)
Enrico Tassi [Fri, 29 Sep 2006 12:49:11 +0000 (12:49 +0000)]
new version of auto that is able to prove the irrationality of sqrt(2)

18 years agoadded tests for auto
Enrico Tassi [Fri, 29 Sep 2006 12:48:07 +0000 (12:48 +0000)]
added tests for auto

18 years agorestored the good factorization file
Enrico Tassi [Fri, 29 Sep 2006 12:47:31 +0000 (12:47 +0000)]
restored the good factorization file

18 years agoported to the new reflexivity implementation
Enrico Tassi [Fri, 29 Sep 2006 12:46:59 +0000 (12:46 +0000)]
ported to the new reflexivity implementation

18 years agomaittaprover uses another format
Enrico Tassi [Fri, 29 Sep 2006 12:23:23 +0000 (12:23 +0000)]
maittaprover uses another format

18 years ago...
Enrico Tassi [Fri, 29 Sep 2006 12:22:36 +0000 (12:22 +0000)]
...

18 years agoremoved a useless printing
Enrico Tassi [Fri, 29 Sep 2006 11:22:39 +0000 (11:22 +0000)]
removed a useless printing

18 years agoadded metas local context maction: ?n[...]
Enrico Tassi [Fri, 29 Sep 2006 11:22:13 +0000 (11:22 +0000)]
added metas local context maction: ?n[...]

18 years agosolved issues regarding SQL incredible error proness
Enrico Tassi [Thu, 28 Sep 2006 14:23:42 +0000 (14:23 +0000)]
solved issues regarding SQL incredible error proness

18 years agoImplemented topological sorting according to the dependencies.
Claudio Sacerdoti Coen [Thu, 28 Sep 2006 11:51:22 +0000 (11:51 +0000)]
Implemented topological sorting according to the dependencies.

18 years agoauto snapshot
Enrico Tassi [Wed, 27 Sep 2006 16:20:40 +0000 (16:20 +0000)]
auto snapshot

18 years ago...
Enrico Tassi [Wed, 27 Sep 2006 16:19:17 +0000 (16:19 +0000)]
...

18 years agoMore work on the translation of technicalities/setoids.ma.
Claudio Sacerdoti Coen [Wed, 27 Sep 2006 15:56:51 +0000 (15:56 +0000)]
More work on the translation of technicalities/setoids.ma.

18 years agoOne less open helps understanding the code!
Claudio Sacerdoti Coen [Wed, 27 Sep 2006 15:50:51 +0000 (15:50 +0000)]
One less open helps understanding the code!

18 years agoMore informative error message.
Claudio Sacerdoti Coen [Wed, 27 Sep 2006 15:04:14 +0000 (15:04 +0000)]
More informative error message.

18 years agofixed bug regarding developments. paths given with -I are now made absolute
Enrico Tassi [Wed, 27 Sep 2006 14:25:10 +0000 (14:25 +0000)]
fixed bug regarding developments. paths given with -I are now made absolute

18 years agoNew bug found in disambiguation of records.
Claudio Sacerdoti Coen [Wed, 27 Sep 2006 13:14:33 +0000 (13:14 +0000)]
New bug found in disambiguation of records.
To fix the bug it is necessary to propagate the substitution computed
during the type-checking of the constructors to the types of the inductive
types. This is quite complex to do. One possibility is simply to add the
substitution to the proof status.

18 years agoInitial work on setoids:
Claudio Sacerdoti Coen [Wed, 27 Sep 2006 09:50:26 +0000 (09:50 +0000)]
Initial work on setoids:
 - AST changed to make it more parametric on terms (for the Relation command)
 - functions that work on ASTs consider the constructors in alphabetical order
 - initial translation from Coq to Matita of library/technicalities/setoids.ma

18 years agoInitial work on setoids:
Claudio Sacerdoti Coen [Wed, 27 Sep 2006 09:49:48 +0000 (09:49 +0000)]
Initial work on setoids:
 - AST changed to make it more parametric on terms (for the Relation command)
 - functions that work on ASTs consider the constructors in alphabetical order
 -

18 years agoAdded generation of dependency graph for the ocaml modules in matita/
Stefano Zacchiroli [Wed, 27 Sep 2006 09:20:29 +0000 (09:20 +0000)]
Added generation of dependency graph for the ocaml modules in matita/
WARNING (and happyness ...): first Ruby script added to our repository

18 years agorebuilt
Stefano Zacchiroli [Wed, 27 Sep 2006 09:19:47 +0000 (09:19 +0000)]
rebuilt

18 years agoTwo tests used to have the same baseuri. Very bad.
Claudio Sacerdoti Coen [Tue, 26 Sep 2006 17:03:57 +0000 (17:03 +0000)]
Two tests used to have the same baseuri. Very bad.

18 years agoadded SRC parameter to makefile (the one placed in the root of a development) to...
Enrico Tassi [Tue, 26 Sep 2006 16:06:54 +0000 (16:06 +0000)]
added SRC parameter to makefile (the one placed in the root of a development) to specify the set of files to handle (if omitted all files reachable from the root dir of the development are used).

18 years agoThe precedence level is now an optional argument of the content to pres
Claudio Sacerdoti Coen [Tue, 26 Sep 2006 11:36:36 +0000 (11:36 +0000)]
The precedence level is now an optional argument of the content to pres
transformation for terms.

18 years agolinkonly now also links matitac
Claudio Sacerdoti Coen [Tue, 26 Sep 2006 11:35:12 +0000 (11:35 +0000)]
linkonly now also links matitac

18 years ago* ocaml => components
Claudio Sacerdoti Coen [Tue, 26 Sep 2006 11:22:08 +0000 (11:22 +0000)]
* ocaml => components
* initialization was missing

18 years agodiscriminate => destruct
Claudio Sacerdoti Coen [Tue, 26 Sep 2006 08:48:08 +0000 (08:48 +0000)]
discriminate => destruct

18 years ago{discriminate,injection} => destruct
Claudio Sacerdoti Coen [Tue, 26 Sep 2006 08:26:17 +0000 (08:26 +0000)]
{discriminate,injection} => destruct

18 years agoinjection_tac and discriminate_tac now replaced by destruct_tac
Claudio Sacerdoti Coen [Mon, 25 Sep 2006 16:54:35 +0000 (16:54 +0000)]
injection_tac and discriminate_tac now replaced by destruct_tac

18 years agoinjection_tac and discriminate_tac now replaced by destruct_tac that
Claudio Sacerdoti Coen [Mon, 25 Sep 2006 16:52:53 +0000 (16:52 +0000)]
injection_tac and discriminate_tac now replaced by destruct_tac that
performs either injection or discrimination. In Coq destruct is called
"analyze equality".

18 years agoSeveral bugs fixed in discriminate.
Claudio Sacerdoti Coen [Mon, 25 Sep 2006 16:07:09 +0000 (16:07 +0000)]
Several bugs fixed in discriminate.
Discriminate now works on inductive types with any number of left or right
parameters.

18 years agoBug fixed: a number alias Num 0 now subsumes the case Num n for each n.
Claudio Sacerdoti Coen [Mon, 25 Sep 2006 14:04:33 +0000 (14:04 +0000)]
Bug fixed: a number alias Num 0 now subsumes the case Num n for each n.

18 years agolast fix.
Enrico Tassi [Sat, 23 Sep 2006 18:09:06 +0000 (18:09 +0000)]
last fix.

18 years agousing lua5.1 instead of lua50
Enrico Tassi [Sat, 23 Sep 2006 16:07:53 +0000 (16:07 +0000)]
using lua5.1 instead of lua50

18 years agooverride USER with bench
Enrico Tassi [Sat, 23 Sep 2006 15:44:45 +0000 (15:44 +0000)]
override USER with bench

18 years agoadded $(USER) so that the night bench can override it (and not put garbage in MY...
Enrico Tassi [Sat, 23 Sep 2006 15:44:14 +0000 (15:44 +0000)]
added $(USER) so that the night bench can override it (and not put garbage in MY sql tables)

18 years agofixed script to make csc happy
Enrico Tassi [Sat, 23 Sep 2006 15:31:09 +0000 (15:31 +0000)]
fixed script to make csc happy

18 years agoBug fixed: aliases for numbers were no longer handled correctly (since 0 was
Claudio Sacerdoti Coen [Fri, 22 Sep 2006 16:28:39 +0000 (16:28 +0000)]
Bug fixed: aliases for numbers were no longer handled correctly (since 0 was
a wildcard only for symbols).

18 years agoauto snapshot
Enrico Tassi [Thu, 21 Sep 2006 16:01:04 +0000 (16:01 +0000)]
auto snapshot

18 years agosnapshot of queries for auto+paramod
Enrico Tassi [Thu, 21 Sep 2006 16:00:31 +0000 (16:00 +0000)]
snapshot of queries for auto+paramod

18 years agoadded notation
Enrico Tassi [Thu, 21 Sep 2006 15:59:21 +0000 (15:59 +0000)]
added notation

18 years ago...
Enrico Tassi [Thu, 21 Sep 2006 15:58:44 +0000 (15:58 +0000)]
...

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