]> matita.cs.unibo.it Git - helm.git/log
helm.git
12 years ago- dynamic type assignment dismissed for now
Ferruccio Guidi [Fri, 13 Jul 2012 16:28:23 +0000 (16:28 +0000)]
- dynamic type assignment dismissed for now
- stratified static type assignment and unwind defined

12 years agocommit by user mkmluser
matitaweb [Tue, 10 Jul 2012 14:33:06 +0000 (14:33 +0000)]
commit by user mkmluser

12 years agocommit by user mkmluser
matitaweb [Tue, 10 Jul 2012 08:55:11 +0000 (08:55 +0000)]
commit by user mkmluser

12 years agocommit by user mkmluser
matitaweb [Tue, 10 Jul 2012 08:54:01 +0000 (08:54 +0000)]
commit by user mkmluser

12 years agomanual commit
matitaweb [Mon, 9 Jul 2012 12:44:27 +0000 (12:44 +0000)]
manual commit

12 years agobug fixes
matitaweb [Sun, 8 Jul 2012 07:19:18 +0000 (07:19 +0000)]
bug fixes

12 years agoreverted to previous version (plus anchors)
matitaweb [Fri, 6 Jul 2012 14:02:50 +0000 (14:02 +0000)]
reverted to previous version (plus anchors)

12 years agoadded tick.png
Wilmer Ricciotti [Fri, 6 Jul 2012 13:27:08 +0000 (13:27 +0000)]
added tick.png

12 years agoAdded NotationPt.name_of_obj.
Wilmer Ricciotti [Fri, 6 Jul 2012 12:39:18 +0000 (12:39 +0000)]
Added NotationPt.name_of_obj.

12 years agoCosmetic changes.
Wilmer Ricciotti [Fri, 6 Jul 2012 12:35:32 +0000 (12:35 +0000)]
Cosmetic changes.

12 years agoBug fixing + cosmetic changes
Wilmer Ricciotti [Fri, 6 Jul 2012 12:32:08 +0000 (12:32 +0000)]
Bug fixing + cosmetic changes

12 years agomanual commit after active hyperlinks
Wilmer Ricciotti [Fri, 6 Jul 2012 12:29:30 +0000 (12:29 +0000)]
manual commit after active hyperlinks

12 years agomanual
Wilmer Ricciotti [Fri, 6 Jul 2012 12:12:46 +0000 (12:12 +0000)]
manual

12 years agocommit by user utente
Wilmer Ricciotti [Fri, 6 Jul 2012 12:03:50 +0000 (12:03 +0000)]
commit by user utente

12 years agoMatitaweb: several improvements in the UI.
Wilmer Ricciotti [Tue, 3 Jul 2012 12:59:02 +0000 (12:59 +0000)]
Matitaweb: several improvements in the UI.

12 years agoMatitaweb: opening a file resets the status.
Wilmer Ricciotti [Tue, 3 Jul 2012 12:58:35 +0000 (12:58 +0000)]
Matitaweb: opening a file resets the status.

12 years agoBug fixed: arguments of a match are (no longer...) in whd; so a function
Claudio Sacerdoti Coen [Fri, 29 Jun 2012 14:25:43 +0000 (14:25 +0000)]
Bug fixed: arguments of a match are (no longer...) in whd; so a function
that expects a term in whd was calling herself recursively on a term not
in whd.

12 years agoNew spec. for advance_both_marks
Andrea Asperti [Thu, 28 Jun 2012 14:49:57 +0000 (14:49 +0000)]
New spec. for advance_both_marks

12 years agoworking on termination
Andrea Asperti [Thu, 28 Jun 2012 13:44:44 +0000 (13:44 +0000)]
working on termination

12 years agoremoved a duplicate
Andrea Asperti [Wed, 27 Jun 2012 09:32:02 +0000 (09:32 +0000)]
removed a duplicate

12 years agoClosed all axioms in turing (but not universal).
Andrea Asperti [Wed, 27 Jun 2012 09:30:52 +0000 (09:30 +0000)]
Closed all axioms in turing (but not universal).
Revised semantics of basic machines for termination
purposes

12 years agoHyperlink support.
Wilmer Ricciotti [Thu, 21 Jun 2012 11:41:16 +0000 (11:41 +0000)]
Hyperlink support.

12 years agoan addition to basic_2
Ferruccio Guidi [Wed, 20 Jun 2012 18:54:06 +0000 (18:54 +0000)]
an addition to basic_2

12 years ago- star.ma: constructor inj of star conflicts with previous constructor
Ferruccio Guidi [Wed, 20 Jun 2012 18:50:32 +0000 (18:50 +0000)]
- star.ma: constructor inj of star conflicts with previous constructor
inj of TC. constructor inj of star renamed to sstep and constructor
injl of starl renamed to sstepl
- lambda_delta: bug fix in reduction rule tpr_zeta which now has the
structure of like tpr_delta. More lemas towards subject reduction of
native typing

12 years agoadv_to_mark_l
Andrea Asperti [Mon, 18 Jun 2012 12:42:50 +0000 (12:42 +0000)]
adv_to_mark_l

12 years agoclosing a few axioms
Andrea Asperti [Mon, 18 Jun 2012 11:14:53 +0000 (11:14 +0000)]
closing a few axioms

12 years agoadditions to basic_2
Ferruccio Guidi [Fri, 15 Jun 2012 21:41:40 +0000 (21:41 +0000)]
additions to basic_2

12 years ago- relation between native type and atomic arity proced
Ferruccio Guidi [Fri, 15 Jun 2012 21:22:03 +0000 (21:22 +0000)]
- relation between native type and atomic arity proced
- higher order native typing defined
- some minor results towards subject reduction for native typing

12 years agomiddot notation
Andrea Asperti [Fri, 15 Jun 2012 11:02:45 +0000 (11:02 +0000)]
middot notation

12 years agoadding match_machines and removing trans_to_tuples
Andrea Asperti [Tue, 12 Jun 2012 15:34:13 +0000 (15:34 +0000)]
adding match_machines and removing trans_to_tuples

12 years agoseveral changes
Andrea Asperti [Tue, 12 Jun 2012 09:46:36 +0000 (09:46 +0000)]
several changes

12 years agoReindented
Claudio Sacerdoti Coen [Mon, 11 Jun 2012 08:29:36 +0000 (08:29 +0000)]
Reindented

12 years agoNew nohyps option for /demod/
Claudio Sacerdoti Coen [Mon, 11 Jun 2012 08:29:15 +0000 (08:29 +0000)]
New nohyps option for /demod/

12 years agoNew flags for demod:
Claudio Sacerdoti Coen [Fri, 8 Jun 2012 17:33:19 +0000 (17:33 +0000)]
New flags for demod:
  1) by ... now can be used to explicitly give the set of equations to use
  2) nohyps can now be used to avoid using the hypotheses

12 years agomove_char.ma
Andrea Asperti [Fri, 8 Jun 2012 11:56:12 +0000 (11:56 +0000)]
move_char.ma
-This line, and those below, will be ignored--

A    turing/move_char.ma

12 years agomerging of char_move_c and char_move_l
Andrea Asperti [Fri, 8 Jun 2012 11:48:47 +0000 (11:48 +0000)]
merging of char_move_c and char_move_l

12 years agoA recompiling version
Andrea Asperti [Fri, 8 Jun 2012 10:49:53 +0000 (10:49 +0000)]
A recompiling version

12 years agoDropping a coercion and some hints due to conflicts with CerCo
Andrea Asperti [Fri, 8 Jun 2012 10:46:29 +0000 (10:46 +0000)]
Dropping a coercion and some hints due to conflicts with CerCo

12 years agoModifications and refactoring
Andrea Asperti [Fri, 8 Jun 2012 09:52:38 +0000 (09:52 +0000)]
Modifications and refactoring

12 years agoMsg reporting via HLogger in the error window made asynchronous => speedup.
Claudio Sacerdoti Coen [Fri, 8 Jun 2012 08:59:06 +0000 (08:59 +0000)]
Msg reporting via HLogger in the error window made asynchronous => speedup.

12 years agoPatch to avoid generating _inv_ind_recTX for X the largest universe.
Claudio Sacerdoti Coen [Thu, 7 Jun 2012 11:53:26 +0000 (11:53 +0000)]
Patch to avoid generating _inv_ind_recTX for X the largest universe.
Rational: for some unknown reason, that takes ages to fail.

12 years agoSys.Break no longer catched
Claudio Sacerdoti Coen [Thu, 7 Jun 2012 11:18:36 +0000 (11:18 +0000)]
Sys.Break no longer catched

12 years agoNew debugging switch in the interface.
Claudio Sacerdoti Coen [Thu, 7 Jun 2012 09:20:27 +0000 (09:20 +0000)]
New debugging switch in the interface.

12 years agoMore conjectures proved.
Wilmer Ricciotti [Wed, 6 Jun 2012 15:34:08 +0000 (15:34 +0000)]
More conjectures proved.

12 years agonew version of move_char_l suign swap
Andrea Asperti [Wed, 6 Jun 2012 09:39:07 +0000 (09:39 +0000)]
new version of move_char_l suign swap

12 years agoswap machine; move_char revisited
Andrea Asperti [Wed, 6 Jun 2012 09:07:48 +0000 (09:07 +0000)]
swap machine; move_char revisited

12 years agorestructuring
Andrea Asperti [Wed, 6 Jun 2012 06:19:48 +0000 (06:19 +0000)]
restructuring

12 years agoRestructuring
Andrea Asperti [Wed, 6 Jun 2012 06:18:43 +0000 (06:18 +0000)]
Restructuring

12 years agoSome results on relations. Moved things around.
Andrea Asperti [Tue, 5 Jun 2012 11:29:18 +0000 (11:29 +0000)]
Some results on relations. Moved things around.

12 years agoCompleted all proofs in if_machine
Andrea Asperti [Tue, 5 Jun 2012 08:22:40 +0000 (08:22 +0000)]
Completed all proofs in if_machine

12 years agoan addition to basic_2
Ferruccio Guidi [Mon, 4 Jun 2012 20:39:26 +0000 (20:39 +0000)]
an addition to basic_2

12 years ago- lambda_delta: subject reduction for nativa type assignment begins ...
Ferruccio Guidi [Mon, 4 Jun 2012 20:34:11 +0000 (20:34 +0000)]
- lambda_delta: subject reduction for nativa type assignment begins ...
                dependecnes between source files improved
- matitadep: little application for optimizing dependences between .ma files
             (used by lambda_delta Makefile)

12 years agosemantics of the if-machine.
Andrea Asperti [Mon, 4 Jun 2012 14:16:05 +0000 (14:16 +0000)]
semantics of the if-machine.
Moved some lemmas to their proper places.

12 years agonotation
Andrea Asperti [Mon, 4 Jun 2012 08:31:30 +0000 (08:31 +0000)]
notation

12 years agocomments
Andrea Asperti [Mon, 4 Jun 2012 06:35:09 +0000 (06:35 +0000)]
comments

12 years agoadditions to basic_2
Ferruccio Guidi [Sat, 2 Jun 2012 18:46:34 +0000 (18:46 +0000)]
additions to basic_2

12 years ago- predefined_virtuals: an addition
Ferruccio Guidi [Sat, 2 Jun 2012 18:37:03 +0000 (18:37 +0000)]
- predefined_virtuals: an addition
- lambda_delta: lenv ref for native type assignment completed
                levn ref for substitution correctly oriented

12 years agoFinalized copy sub-machine of the universal turing machine. Some new results
Wilmer Ricciotti [Fri, 1 Jun 2012 14:40:49 +0000 (14:40 +0000)]
Finalized copy sub-machine of the universal turing machine. Some new results
on lists.

12 years agoCi siamo quasi
Andrea Asperti [Fri, 1 Jun 2012 12:53:28 +0000 (12:53 +0000)]
Ci siamo quasi

12 years agoupdate in basic_2
Ferruccio Guidi [Fri, 1 Jun 2012 12:36:29 +0000 (12:36 +0000)]
update in basic_2

12 years ago- predefined_virtuals: some additions
Ferruccio Guidi [Fri, 1 Jun 2012 12:34:16 +0000 (12:34 +0000)]
- predefined_virtuals: some additions
- lambda_delta: first results on lenv. ref. for native typing
                some notational changes

12 years agoThanks to Guarrigue, code for Serializer functor simplified using
Claudio Sacerdoti Coen [Thu, 31 May 2012 13:52:13 +0000 (13:52 +0000)]
Thanks to Guarrigue, code for Serializer functor simplified using
private types. The type system of OCaml is more and more misterious...

12 years agoProgress.
Wilmer Ricciotti [Thu, 31 May 2012 10:51:18 +0000 (10:51 +0000)]
Progress.

12 years agoupdate in basic_2
Ferruccio Guidi [Wed, 30 May 2012 21:12:25 +0000 (21:12 +0000)]
update in basic_2

12 years ago- nDestructTac: Sys.break handled in two places
Ferruccio Guidi [Wed, 30 May 2012 21:10:44 +0000 (21:10 +0000)]
- nDestructTac: Sys.break handled in two places
- lambda_delta: a major property of native type assignment
                some properties of context sensitive equivalence
some notational changes
some annotations

12 years agoProgress.
Wilmer Ricciotti [Wed, 30 May 2012 14:20:28 +0000 (14:20 +0000)]
Progress.

12 years agosome progress
Andrea Asperti [Wed, 30 May 2012 11:56:33 +0000 (11:56 +0000)]
some progress

12 years agoProgress.
Wilmer Ricciotti [Wed, 30 May 2012 09:11:08 +0000 (09:11 +0000)]
Progress.

12 years agoProgress.
Wilmer Ricciotti [Wed, 30 May 2012 08:35:51 +0000 (08:35 +0000)]
Progress.

12 years agoThe universal machine!!!
Andrea Asperti [Tue, 29 May 2012 14:01:20 +0000 (14:01 +0000)]
The universal machine!!!

12 years agotrans_step.ma
Andrea Asperti [Mon, 28 May 2012 16:42:25 +0000 (16:42 +0000)]
trans_step.ma

12 years agoporting move_tape.ma
Andrea Asperti [Mon, 28 May 2012 14:02:42 +0000 (14:02 +0000)]
porting move_tape.ma

12 years agoporting move_char_l.ma
Andrea Asperti [Mon, 28 May 2012 13:47:38 +0000 (13:47 +0000)]
porting move_char_l.ma

12 years agoporting of move_char_c
Andrea Asperti [Mon, 28 May 2012 13:33:45 +0000 (13:33 +0000)]
porting of move_char_c

12 years agomore typos
Andrea Asperti [Mon, 28 May 2012 12:13:49 +0000 (12:13 +0000)]
more typos

12 years agotypos
Andrea Asperti [Mon, 28 May 2012 12:11:59 +0000 (12:11 +0000)]
typos

12 years agograph of a function
Andrea Asperti [Mon, 28 May 2012 11:42:02 +0000 (11:42 +0000)]
graph of a function

12 years agoFinOpt
Andrea Asperti [Mon, 28 May 2012 11:25:09 +0000 (11:25 +0000)]
FinOpt

12 years agomem, split
Andrea Asperti [Mon, 28 May 2012 06:21:26 +0000 (06:21 +0000)]
mem, split

12 years agoProgress.
Wilmer Ricciotti [Mon, 28 May 2012 06:19:50 +0000 (06:19 +0000)]
Progress.

12 years agotentative specification of Conway's construction for surreal numbers
Ferruccio Guidi [Sat, 26 May 2012 12:47:48 +0000 (12:47 +0000)]
tentative specification of Conway's construction for surreal numbers
matita.opt game.ma crashes after 4 lines of code :((

12 years agoupdate in basic_2
Ferruccio Guidi [Fri, 25 May 2012 17:16:04 +0000 (17:16 +0000)]
update in basic_2

12 years ago- substitution lemma for native type assignmenr proved!
Ferruccio Guidi [Fri, 25 May 2012 17:10:54 +0000 (17:10 +0000)]
- substitution lemma for native type assignmenr proved!
- notation change in the support for abstract c.r.'s
- some minor additions

12 years agoProgress
Wilmer Ricciotti [Fri, 25 May 2012 16:15:31 +0000 (16:15 +0000)]
Progress

12 years agoPorting to the new defintion of finset
Andrea Asperti [Fri, 25 May 2012 08:59:21 +0000 (08:59 +0000)]
Porting to the new defintion of finset

12 years agoNew definition of finset.
Andrea Asperti [Fri, 25 May 2012 08:58:36 +0000 (08:58 +0000)]
New definition of finset.

12 years agoa bit faster
Andrea Asperti [Fri, 25 May 2012 07:12:54 +0000 (07:12 +0000)]
a bit faster

12 years agoProgress
Wilmer Ricciotti [Thu, 24 May 2012 15:15:14 +0000 (15:15 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Thu, 24 May 2012 09:52:31 +0000 (09:52 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Wed, 23 May 2012 14:32:15 +0000 (14:32 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Wed, 23 May 2012 09:52:17 +0000 (09:52 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Tue, 22 May 2012 16:07:23 +0000 (16:07 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Tue, 22 May 2012 14:27:50 +0000 (14:27 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Tue, 22 May 2012 09:50:14 +0000 (09:50 +0000)]
Progress

12 years agoProgress.
Wilmer Ricciotti [Mon, 21 May 2012 16:57:38 +0000 (16:57 +0000)]
Progress.

12 years agoAdded move_tape.ma
Wilmer Ricciotti [Mon, 21 May 2012 11:57:26 +0000 (11:57 +0000)]
Added move_tape.ma

12 years agoProgress
Wilmer Ricciotti [Mon, 21 May 2012 11:57:00 +0000 (11:57 +0000)]
Progress

12 years agoNew version of init copy
Andrea Asperti [Mon, 21 May 2012 09:12:57 +0000 (09:12 +0000)]
New version of init copy

12 years agoProgress
Wilmer Ricciotti [Fri, 18 May 2012 16:30:03 +0000 (16:30 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Fri, 18 May 2012 15:43:37 +0000 (15:43 +0000)]
Progress