]>
matita.cs.unibo.it Git - helm.git/log
Andrea Asperti [Mon, 19 Nov 2007 11:55:54 +0000 (11:55 +0000)]
Towards chebyshev.
Claudio Sacerdoti Coen [Sun, 18 Nov 2007 18:18:02 +0000 (18:18 +0000)]
The axiom can be proved. Just follow the hint.
Enrico Tassi [Sat, 17 Nov 2007 18:27:15 +0000 (18:27 +0000)]
fixed bugs found by csc
Enrico Tassi [Sat, 17 Nov 2007 17:33:43 +0000 (17:33 +0000)]
moved to pkg-ocaml-maint
Claudio Sacerdoti Coen [Fri, 16 Nov 2007 20:49:49 +0000 (20:49 +0000)]
Some notes for Enrico.
Enrico Tassi [Fri, 16 Nov 2007 19:39:34 +0000 (19:39 +0000)]
...
Enrico Tassi [Fri, 16 Nov 2007 19:34:32 +0000 (19:34 +0000)]
hidded publish-devel button, too dangerous for the casual user
Enrico Tassi [Fri, 16 Nov 2007 19:32:12 +0000 (19:32 +0000)]
hidded all hbugs related stuff
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
Enrico Tassi [Fri, 16 Nov 2007 18:36:44 +0000 (18:36 +0000)]
...
Enrico Tassi [Fri, 16 Nov 2007 14:34:33 +0000 (14:34 +0000)]
...
Enrico Tassi [Fri, 16 Nov 2007 14:24:38 +0000 (14:24 +0000)]
nocomposites
Enrico Tassi [Fri, 16 Nov 2007 14:24:24 +0000 (14:24 +0000)]
compose tactic restore and added nocomposites keyword
Enrico Tassi [Fri, 16 Nov 2007 14:12:48 +0000 (14:12 +0000)]
more cleanup
Enrico Tassi [Fri, 16 Nov 2007 11:15:04 +0000 (11:15 +0000)]
...
Enrico Tassi [Fri, 16 Nov 2007 10:21:11 +0000 (10:21 +0000)]
added recommends graphvi
Enrico Tassi [Fri, 16 Nov 2007 10:10:11 +0000 (10:10 +0000)]
...
Enrico Tassi [Fri, 16 Nov 2007 10:08:08 +0000 (10:08 +0000)]
xxx
Enrico Tassi [Fri, 16 Nov 2007 10:02:48 +0000 (10:02 +0000)]
added homepage field in control
Enrico Tassi [Fri, 16 Nov 2007 09:56:38 +0000 (09:56 +0000)]
fix
Enrico Tassi [Fri, 16 Nov 2007 09:33:37 +0000 (09:33 +0000)]
fix -noinnertypes set to true!
Enrico Tassi [Fri, 16 Nov 2007 09:11:50 +0000 (09:11 +0000)]
removed dummy MATITA_CFLAGS assignement
Enrico Tassi [Fri, 16 Nov 2007 09:04:05 +0000 (09:04 +0000)]
added default for matita.noiinertypes
Enrico Tassi [Fri, 16 Nov 2007 08:56:55 +0000 (08:56 +0000)]
menu fised
Enrico Tassi [Fri, 16 Nov 2007 08:51:34 +0000 (08:51 +0000)]
propagation of noinnertypes to matitac
Enrico Tassi [Fri, 16 Nov 2007 08:49:23 +0000 (08:49 +0000)]
added -noinnertypes
Enrico Tassi [Fri, 16 Nov 2007 08:06:40 +0000 (08:06 +0000)]
...
Enrico Tassi [Thu, 15 Nov 2007 17:15:05 +0000 (17:15 +0000)]
cleanup
Enrico Tassi [Thu, 15 Nov 2007 17:14:37 +0000 (17:14 +0000)]
cleanup
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 #
Enrico Tassi [Thu, 15 Nov 2007 16:35:08 +0000 (16:35 +0000)]
...
Enrico Tassi [Thu, 15 Nov 2007 15:35:16 +0000 (15:35 +0000)]
autobatch => [auto]
Enrico Tassi [Thu, 15 Nov 2007 15:27:54 +0000 (15:27 +0000)]
...
Enrico Tassi [Thu, 15 Nov 2007 15:22:23 +0000 (15:22 +0000)]
...
Enrico Tassi [Thu, 15 Nov 2007 13:44:43 +0000 (13:44 +0000)]
removed prerr_endline
Enrico Tassi [Thu, 15 Nov 2007 13:33:53 +0000 (13:33 +0000)]
removed ugly prerr_endline
Enrico Tassi [Thu, 15 Nov 2007 13:22:41 +0000 (13:22 +0000)]
added --version to allow help2man
Enrico Tassi [Thu, 15 Nov 2007 13:22:13 +0000 (13:22 +0000)]
added manpages
Enrico Tassi [Thu, 15 Nov 2007 11:07:14 +0000 (11:07 +0000)]
...
Enrico Tassi [Thu, 15 Nov 2007 11:06:31 +0000 (11:06 +0000)]
matita-icon
Enrico Tassi [Thu, 15 Nov 2007 10:45:04 +0000 (10:45 +0000)]
...
Enrico Tassi [Thu, 15 Nov 2007 10:44:45 +0000 (10:44 +0000)]
...
Enrico Tassi [Thu, 15 Nov 2007 10:31:06 +0000 (10:31 +0000)]
...
Enrico Tassi [Thu, 15 Nov 2007 10:30:21 +0000 (10:30 +0000)]
wrong dependency removed
Enrico Tassi [Thu, 15 Nov 2007 09:34:25 +0000 (09:34 +0000)]
changelog to -rc-1
Enrico Tassi [Thu, 15 Nov 2007 09:33:08 +0000 (09:33 +0000)]
...
Enrico Tassi [Thu, 15 Nov 2007 09:21:09 +0000 (09:21 +0000)]
rc-1
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.
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.
Enrico Tassi [Wed, 14 Nov 2007 22:36:35 +0000 (22:36 +0000)]
xxx
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
Enrico Tassi [Wed, 14 Nov 2007 13:21:06 +0000 (13:21 +0000)]
fixed notation
Enrico Tassi [Wed, 14 Nov 2007 13:17:07 +0000 (13:17 +0000)]
ogroups almost finished
Enrico Tassi [Wed, 14 Nov 2007 12:42:28 +0000 (12:42 +0000)]
snapshot
Enrico Tassi [Wed, 14 Nov 2007 09:11:48 +0000 (09:11 +0000)]
snapshot
Enrico Tassi [Tue, 13 Nov 2007 17:52:09 +0000 (17:52 +0000)]
End of groups :-)
Enrico Tassi [Tue, 13 Nov 2007 16:40:43 +0000 (16:40 +0000)]
snapshot
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
Ferruccio Guidi [Tue, 13 Nov 2007 10:35:09 +0000 (10:35 +0000)]
previously hidden simplifications (in old destruct) added
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
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
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
Enrico Tassi [Mon, 12 Nov 2007 16:42:19 +0000 (16:42 +0000)]
removed ugly printing
Enrico Tassi [Mon, 12 Nov 2007 16:41:30 +0000 (16:41 +0000)]
ordered_sets are built with excedence
Enrico Tassi [Mon, 12 Nov 2007 16:41:02 +0000 (16:41 +0000)]
added ordered sets
Enrico Tassi [Mon, 12 Nov 2007 16:40:30 +0000 (16:40 +0000)]
renamed ordered sets into excedence.ma
Enrico Tassi [Mon, 12 Nov 2007 16:39:44 +0000 (16:39 +0000)]
relocated
Enrico Tassi [Mon, 12 Nov 2007 16:38:46 +0000 (16:38 +0000)]
removed dust
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
Enrico Tassi [Mon, 12 Nov 2007 15:22:59 +0000 (15:22 +0000)]
new file with some relations stated in Type
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.
Ferruccio Guidi [Mon, 12 Nov 2007 12:35:56 +0000 (12:35 +0000)]
refactoring
Ferruccio Guidi [Sat, 10 Nov 2007 16:54:55 +0000 (16:54 +0000)]
old subst tactics removed. New destruct tactic used instead
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.
Claudio Sacerdoti Coen [Sat, 10 Nov 2007 13:16:57 +0000 (13:16 +0000)]
More correct (but still bugged) implementation of type definition.
Claudio Sacerdoti Coen [Sat, 10 Nov 2007 11:05:00 +0000 (11:05 +0000)]
Dead code removed.
More ocaml keywords.
Enrico Tassi [Fri, 9 Nov 2007 13:37:05 +0000 (13:37 +0000)]
snapshot
Enrico Tassi [Fri, 9 Nov 2007 08:39:33 +0000 (08:39 +0000)]
...
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
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 21:46:15 +0000 (21:46 +0000)]
Trivial bug fixed in type inference of LetIn source types.
Enrico Tassi [Thu, 8 Nov 2007 17:03:23 +0000 (17:03 +0000)]
xxx
Enrico Tassi [Thu, 8 Nov 2007 14:54:31 +0000 (14:54 +0000)]
ported to the new destruct
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.
Claudio Sacerdoti Coen [Thu, 8 Nov 2007 14:02:56 +0000 (14:02 +0000)]
svn:ignore set
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
Enrico Tassi [Thu, 8 Nov 2007 12:28:12 +0000 (12:28 +0000)]
forced associativity in if construct
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.
Ferruccio Guidi [Wed, 7 Nov 2007 20:24:34 +0000 (20:24 +0000)]
set svn:ignore to *.ml in the deve directories
Ferruccio Guidi [Wed, 7 Nov 2007 19:52:14 +0000 (19:52 +0000)]
- bug fix in destruct
- old subst tactic removed
- some tests fixed
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
Enrico Tassi [Wed, 7 Nov 2007 14:39:07 +0000 (14:39 +0000)]
Code extraction unbranched again.
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)
Claudio Sacerdoti Coen [Tue, 6 Nov 2007 12:29:13 +0000 (12:29 +0000)]
cic_acic should be compiled before cic_exportation
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).
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.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 14:29:47 +0000 (14:29 +0000)]
Obj.magic are now generated to extract dependently typed MutCases.
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.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 12:18:15 +0000 (12:18 +0000)]
Slightly nicer output.
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.
Claudio Sacerdoti Coen [Mon, 5 Nov 2007 10:10:33 +0000 (10:10 +0000)]
Type application and abstractions are now exported correctly.