]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agoTowards chebyshev.
Andrea Asperti [Mon, 19 Nov 2007 11:55:54 +0000 (11:55 +0000)]
Towards chebyshev.

16 years agoThe axiom can be proved. Just follow the hint.
Claudio Sacerdoti Coen [Sun, 18 Nov 2007 18:18:02 +0000 (18:18 +0000)]
The axiom can be proved. Just follow the hint.

16 years agofixed bugs found by csc
Enrico Tassi [Sat, 17 Nov 2007 18:27:15 +0000 (18:27 +0000)]
fixed bugs found by csc

16 years agomoved to pkg-ocaml-maint
Enrico Tassi [Sat, 17 Nov 2007 17:33:43 +0000 (17:33 +0000)]
moved to pkg-ocaml-maint

16 years agoSome notes for Enrico.
Claudio Sacerdoti Coen [Fri, 16 Nov 2007 20:49:49 +0000 (20:49 +0000)]
Some notes for Enrico.

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 19:39:34 +0000 (19:39 +0000)]
...

16 years agohidded publish-devel button, too dangerous for the casual user
Enrico Tassi [Fri, 16 Nov 2007 19:34:32 +0000 (19:34 +0000)]
hidded publish-devel button, too dangerous for the casual user

16 years agohidded all hbugs related stuff
Enrico Tassi [Fri, 16 Nov 2007 19:32:12 +0000 (19:32 +0000)]
hidded all hbugs related stuff

16 years agofrom the tarball removed all contribs, they used to weight more than 1MB
Enrico Tassi [Fri, 16 Nov 2007 18:47:49 +0000 (18:47 +0000)]
from the tarball removed all contribs, they used to weight more than 1MB
and were not compiled nor installed

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 18:36:44 +0000 (18:36 +0000)]
...

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 14:34:33 +0000 (14:34 +0000)]
...

16 years agonocomposites
Enrico Tassi [Fri, 16 Nov 2007 14:24:38 +0000 (14:24 +0000)]
nocomposites

16 years agocompose tactic restore and added nocomposites keyword
Enrico Tassi [Fri, 16 Nov 2007 14:24:24 +0000 (14:24 +0000)]
compose tactic restore and added nocomposites keyword

16 years agomore cleanup
Enrico Tassi [Fri, 16 Nov 2007 14:12:48 +0000 (14:12 +0000)]
more cleanup

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 11:15:04 +0000 (11:15 +0000)]
...

16 years agoadded recommends graphvi
Enrico Tassi [Fri, 16 Nov 2007 10:21:11 +0000 (10:21 +0000)]
added recommends graphvi

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 10:10:11 +0000 (10:10 +0000)]
...

16 years agoxxx
Enrico Tassi [Fri, 16 Nov 2007 10:08:08 +0000 (10:08 +0000)]
xxx

16 years agoadded homepage field in control
Enrico Tassi [Fri, 16 Nov 2007 10:02:48 +0000 (10:02 +0000)]
added homepage field in control

16 years agofix
Enrico Tassi [Fri, 16 Nov 2007 09:56:38 +0000 (09:56 +0000)]
fix

16 years agofix -noinnertypes set to true!
Enrico Tassi [Fri, 16 Nov 2007 09:33:37 +0000 (09:33 +0000)]
fix -noinnertypes set to true!

16 years agoremoved dummy MATITA_CFLAGS assignement
Enrico Tassi [Fri, 16 Nov 2007 09:11:50 +0000 (09:11 +0000)]
removed dummy MATITA_CFLAGS assignement

16 years agoadded default for matita.noiinertypes
Enrico Tassi [Fri, 16 Nov 2007 09:04:05 +0000 (09:04 +0000)]
added default for matita.noiinertypes

16 years agomenu fised
Enrico Tassi [Fri, 16 Nov 2007 08:56:55 +0000 (08:56 +0000)]
menu fised

16 years agopropagation of noinnertypes to matitac
Enrico Tassi [Fri, 16 Nov 2007 08:51:34 +0000 (08:51 +0000)]
propagation of noinnertypes to matitac

16 years agoadded -noinnertypes
Enrico Tassi [Fri, 16 Nov 2007 08:49:23 +0000 (08:49 +0000)]
added -noinnertypes

16 years ago...
Enrico Tassi [Fri, 16 Nov 2007 08:06:40 +0000 (08:06 +0000)]
...

16 years agocleanup
Enrico Tassi [Thu, 15 Nov 2007 17:15:05 +0000 (17:15 +0000)]
cleanup

16 years agocleanup
Enrico Tassi [Thu, 15 Nov 2007 17:14:37 +0000 (17:14 +0000)]
cleanup

16 years agodeclared eq_sym as a coercion and added 2 lemmas for rewriting #
Enrico Tassi [Thu, 15 Nov 2007 17:13:51 +0000 (17:13 +0000)]
declared eq_sym as a coercion and added 2 lemmas for rewriting #

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 16:35:08 +0000 (16:35 +0000)]
...

16 years agoautobatch => [auto]
Enrico Tassi [Thu, 15 Nov 2007 15:35:16 +0000 (15:35 +0000)]
autobatch => [auto]

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 15:27:54 +0000 (15:27 +0000)]
...

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 15:22:23 +0000 (15:22 +0000)]
...

16 years agoremoved prerr_endline
Enrico Tassi [Thu, 15 Nov 2007 13:44:43 +0000 (13:44 +0000)]
removed prerr_endline

16 years agoremoved ugly prerr_endline
Enrico Tassi [Thu, 15 Nov 2007 13:33:53 +0000 (13:33 +0000)]
removed ugly prerr_endline

16 years agoadded --version to allow help2man
Enrico Tassi [Thu, 15 Nov 2007 13:22:41 +0000 (13:22 +0000)]
added --version to allow help2man

16 years agoadded manpages
Enrico Tassi [Thu, 15 Nov 2007 13:22:13 +0000 (13:22 +0000)]
added manpages

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 11:07:14 +0000 (11:07 +0000)]
...

16 years agomatita-icon
Enrico Tassi [Thu, 15 Nov 2007 11:06:31 +0000 (11:06 +0000)]
matita-icon

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 10:45:04 +0000 (10:45 +0000)]
...

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 10:44:45 +0000 (10:44 +0000)]
...

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 10:31:06 +0000 (10:31 +0000)]
...

16 years agowrong dependency removed
Enrico Tassi [Thu, 15 Nov 2007 10:30:21 +0000 (10:30 +0000)]
wrong dependency removed

16 years agochangelog to -rc-1
Enrico Tassi [Thu, 15 Nov 2007 09:34:25 +0000 (09:34 +0000)]
changelog to -rc-1

16 years ago...
Enrico Tassi [Thu, 15 Nov 2007 09:33:08 +0000 (09:33 +0000)]
...

16 years agorc-1
Enrico Tassi [Thu, 15 Nov 2007 09:21:09 +0000 (09:21 +0000)]
rc-1

16 years agoadded ~delta parameter to saturate_term and used it when saturating a coercion.
Enrico Tassi [Thu, 15 Nov 2007 09:20:34 +0000 (09:20 +0000)]
added ~delta parameter to saturate_term and used it when saturating a coercion.
it is always true that the user wants the type of its coercion no to be
unfolded, since its arity was computed without unfolding.

16 years agoBug fixed: yet another case where tys of mutual recursive functions were not
Claudio Sacerdoti Coen [Wed, 14 Nov 2007 23:20:37 +0000 (23:20 +0000)]
Bug fixed: yet another case where tys of mutual recursive functions were not
lifted correctly when pushed in the context.

16 years agoxxx
Enrico Tassi [Wed, 14 Nov 2007 22:36:35 +0000 (22:36 +0000)]
xxx

16 years agonow destruct takes an optional list of term rather than a sigle optional term
Ferruccio Guidi [Wed, 14 Nov 2007 20:28:58 +0000 (20:28 +0000)]
now destruct takes an optional list of term rather than a sigle optional term

16 years agofixed notation
Enrico Tassi [Wed, 14 Nov 2007 13:21:06 +0000 (13:21 +0000)]
fixed notation

16 years agoogroups almost finished
Enrico Tassi [Wed, 14 Nov 2007 13:17:07 +0000 (13:17 +0000)]
ogroups almost finished

16 years agosnapshot
Enrico Tassi [Wed, 14 Nov 2007 12:42:28 +0000 (12:42 +0000)]
snapshot

16 years agosnapshot
Enrico Tassi [Wed, 14 Nov 2007 09:11:48 +0000 (09:11 +0000)]
snapshot

16 years agoEnd of groups :-)
Enrico Tassi [Tue, 13 Nov 2007 17:52:09 +0000 (17:52 +0000)]
End of groups :-)

16 years agosnapshot
Enrico Tassi [Tue, 13 Nov 2007 16:40:43 +0000 (16:40 +0000)]
snapshot

16 years ago- ProofEngineHelpers: namer_of moved to GrafiteEngine
Ferruccio Guidi [Tue, 13 Nov 2007 16:28:34 +0000 (16:28 +0000)]
- ProofEngineHelpers: namer_of moved to GrafiteEngine
- DestructTactic: unexported destruct_tac now uses lazy terms

16 years agopreviously hidden simplifications (in old destruct) added
Ferruccio Guidi [Tue, 13 Nov 2007 10:35:09 +0000 (10:35 +0000)]
previously hidden simplifications (in old destruct) added

16 years agosome work till the need of redoing all groups based on excedence
Enrico Tassi [Mon, 12 Nov 2007 22:23:36 +0000 (22:23 +0000)]
some work till the need of redoing all groups based on excedence

16 years agosince there is no more tab, the modification of the current file is in the window...
Enrico Tassi [Mon, 12 Nov 2007 21:14:49 +0000 (21:14 +0000)]
since there is no more tab, the modification of the current file is in the window title

16 years ago- destruct tactic: automatic simplification in case of failure removed
Ferruccio Guidi [Mon, 12 Nov 2007 18:35:12 +0000 (18:35 +0000)]
- destruct tactic: automatic simplification in case of failure removed
- library scripts: changed accordingly
- LOGIC: injection lemmas for the coercions added and applied where neaded

Note: destruct does not whd the equality argument as the old subst did

16 years agoremoved ugly printing
Enrico Tassi [Mon, 12 Nov 2007 16:42:19 +0000 (16:42 +0000)]
removed ugly printing

16 years agoordered_sets are built with excedence
Enrico Tassi [Mon, 12 Nov 2007 16:41:30 +0000 (16:41 +0000)]
ordered_sets are built with excedence

16 years agoadded ordered sets
Enrico Tassi [Mon, 12 Nov 2007 16:41:02 +0000 (16:41 +0000)]
added ordered sets

16 years agorenamed ordered sets into excedence.ma
Enrico Tassi [Mon, 12 Nov 2007 16:40:30 +0000 (16:40 +0000)]
renamed ordered sets into excedence.ma

16 years agorelocated
Enrico Tassi [Mon, 12 Nov 2007 16:39:44 +0000 (16:39 +0000)]
relocated

16 years agoremoved dust
Enrico Tassi [Mon, 12 Nov 2007 16:38:46 +0000 (16:38 +0000)]
removed dust

16 years agoHIDDEN (since glade do not read out file properly anymore) tactic bar and
Enrico Tassi [Mon, 12 Nov 2007 16:38:25 +0000 (16:38 +0000)]
HIDDEN (since glade do not read out file properly anymore) tactic bar and
outline notebook tab

16 years agonew file with some relations stated in Type
Enrico Tassi [Mon, 12 Nov 2007 15:22:59 +0000 (15:22 +0000)]
new file with some relations stated in Type

16 years agoordered set is over, much new stuff coming from a coreflexivee/cotransitive
Enrico Tassi [Mon, 12 Nov 2007 15:22:43 +0000 (15:22 +0000)]
ordered set is over, much new stuff coming from a coreflexivee/cotransitive
execedence relation.

16 years agorefactoring
Ferruccio Guidi [Mon, 12 Nov 2007 12:35:56 +0000 (12:35 +0000)]
refactoring

16 years agoold subst tactics removed. New destruct tactic used instead
Ferruccio Guidi [Sat, 10 Nov 2007 16:54:55 +0000 (16:54 +0000)]
old subst tactics removed. New destruct tactic used instead

16 years agoa) Detection of existential types now implemented
Claudio Sacerdoti Coen [Sat, 10 Nov 2007 14:07:13 +0000 (14:07 +0000)]
a) Detection of existential types now implemented
b) New heuristic for pretty printing of type definition arguments.

16 years agoMore correct (but still bugged) implementation of type definition.
Claudio Sacerdoti Coen [Sat, 10 Nov 2007 13:16:57 +0000 (13:16 +0000)]
More correct (but still bugged) implementation of type definition.

16 years agoDead code removed.
Claudio Sacerdoti Coen [Sat, 10 Nov 2007 11:05:00 +0000 (11:05 +0000)]
Dead code removed.
More ocaml keywords.

17 years agosnapshot
Enrico Tassi [Fri, 9 Nov 2007 13:37:05 +0000 (13:37 +0000)]
snapshot

17 years ago...
Enrico Tassi [Fri, 9 Nov 2007 08:39:33 +0000 (08:39 +0000)]
...

17 years ago- subst tactic keyword removed from highlight syntax tables
Ferruccio Guidi [Thu, 8 Nov 2007 22:01:54 +0000 (22:01 +0000)]
- subst tactic keyword removed from highlight syntax tables
- svn:ignore property fixed for Base-2 devel

17 years agoTrivial bug fixed in type inference of LetIn source types.
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 21:46:15 +0000 (21:46 +0000)]
Trivial bug fixed in type inference of LetIn source types.

17 years agoxxx
Enrico Tassi [Thu, 8 Nov 2007 17:03:23 +0000 (17:03 +0000)]
xxx

17 years agoported to the new destruct
Enrico Tassi [Thu, 8 Nov 2007 14:54:31 +0000 (14:54 +0000)]
ported to the new destruct

17 years agoArguments of constructors in a case pattern are now ppid-ed.
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 14:06:13 +0000 (14:06 +0000)]
Arguments of constructors in a case pattern are now ppid-ed.

17 years agosvn:ignore set
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 14:02:56 +0000 (14:02 +0000)]
svn:ignore set

17 years agoplease, commit files with debug=false otherwise the distributed matita prints a ton...
Enrico Tassi [Thu, 8 Nov 2007 12:33:11 +0000 (12:33 +0000)]
please, commit files with debug=false otherwise the distributed matita prints a ton of dust

17 years agoforced associativity in if construct
Enrico Tassi [Thu, 8 Nov 2007 12:28:12 +0000 (12:28 +0000)]
forced associativity in if construct

17 years agoZoli's note (in Italian) about a constructive version of Lebesgue's dominated
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 08:43:02 +0000 (08:43 +0000)]
Zoli's note (in Italian) about a constructive version of Lebesgue's dominated
convergence theorem in a point-free setting.

17 years agoset svn:ignore to *.ml in the deve directories
Ferruccio Guidi [Wed, 7 Nov 2007 20:24:34 +0000 (20:24 +0000)]
set svn:ignore to *.ml in the deve directories

17 years ago- bug fix in destruct
Ferruccio Guidi [Wed, 7 Nov 2007 19:52:14 +0000 (19:52 +0000)]
- bug fix in destruct
- old subst tactic removed
- some tests fixed

17 years agoreorganization of the whole story, the root dir contains the algebraic structure
Enrico Tassi [Wed, 7 Nov 2007 14:44:24 +0000 (14:44 +0000)]
reorganization of the whole story, the root dir contains the algebraic structure

17 years agoCode extraction unbranched again.
Enrico Tassi [Wed, 7 Nov 2007 14:39:07 +0000 (14:39 +0000)]
Code extraction unbranched again.

17 years agonew implementation of the destruct tactic,
Ferruccio Guidi [Tue, 6 Nov 2007 19:30:16 +0000 (19:30 +0000)]
new implementation of the destruct tactic,
which includes the old subst tactic (now removed)

17 years agocic_acic should be compiled before cic_exportation
Claudio Sacerdoti Coen [Tue, 6 Nov 2007 12:29:13 +0000 (12:29 +0000)]
cic_acic should be compiled before cic_exportation

17 years agoBug in detection of too polymorphic types partially fixed (see comment).
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 15:14:23 +0000 (15:14 +0000)]
Bug in detection of too polymorphic types partially fixed (see comment).

17 years agoMutCases that occur in types should be handled with "any type".
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 14:56:16 +0000 (14:56 +0000)]
MutCases that occur in types should be handled with "any type".
Unfortunately, such type does not exists in OCaml. For now I generate
unit with a comment. Applications to arguments will fail and require another
Obj.magic.

17 years agoObj.magic are now generated to extract dependently typed MutCases.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 14:29:47 +0000 (14:29 +0000)]
Obj.magic are now generated to extract dependently typed MutCases.

17 years agoHandling of left parameters of constructors/indutive type definitions improved.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 14:20:20 +0000 (14:20 +0000)]
Handling of left parameters of constructors/indutive type definitions improved.
Bug fixed: arguments of sort Prop were not dropped from MutCase branches.

17 years agoSlightly nicer output.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 12:18:15 +0000 (12:18 +0000)]
Slightly nicer output.

17 years agoFilenames are now fully mangled (e.g. matita_nat_nat.ml) to avoid file name
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 12:10:34 +0000 (12:10 +0000)]
Filenames are now fully mangled (e.g. matita_nat_nat.ml) to avoid file name
clashes.

17 years agoType application and abstractions are now exported correctly.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 10:10:33 +0000 (10:10 +0000)]
Type application and abstractions are now exported correctly.