]> matita.cs.unibo.it Git - helm.git/log
helm.git
8 years agowork in progress on frees_drops
Ferruccio Guidi [Mon, 6 Jun 2016 20:20:44 +0000 (20:20 +0000)]
work in progress on frees_drops

8 years agoMaTeX:
Ferruccio Guidi [Mon, 6 Jun 2016 15:39:21 +0000 (15:39 +0000)]
MaTeX:
- notational macros for constants
- notational macro for quantification of propositions
matex.sty:
- support for math mode
- improved rendering of basic constructions
test style sheets
- some notational macros for legacy_1

8 years ago- source web pages for lambdadelta_1
Ferruccio Guidi [Wed, 1 Jun 2016 14:33:30 +0000 (14:33 +0000)]
- source web pages for lambdadelta_1
- minor bugs fixed in the web site

8 years ago- update in ground_2 and basic_2
Ferruccio Guidi [Tue, 31 May 2016 19:19:40 +0000 (19:19 +0000)]
- update in ground_2 and basic_2
- updated documentation

8 years agofrees_drops, initial versrion
Ferruccio Guidi [Tue, 31 May 2016 19:06:53 +0000 (19:06 +0000)]
frees_drops, initial versrion

8 years agosome results on co-composition ...
Ferruccio Guidi [Mon, 30 May 2016 18:57:34 +0000 (18:57 +0000)]
some results on co-composition ...

8 years agomore results on sor ...
Ferruccio Guidi [Sun, 29 May 2016 18:13:10 +0000 (18:13 +0000)]
more results on sor ...

8 years agoinitial support for lfpx_drops ...
Ferruccio Guidi [Wed, 25 May 2016 12:12:25 +0000 (12:12 +0000)]
initial support for lfpx_drops ...

8 years agomore files missing :((
Ferruccio Guidi [Tue, 24 May 2016 19:05:12 +0000 (19:05 +0000)]
more files missing :((

8 years agoune file was missing :(
Ferruccio Guidi [Tue, 24 May 2016 19:04:08 +0000 (19:04 +0000)]
une file was missing :(

8 years agobug fixing ...
Ferruccio Guidi [Tue, 24 May 2016 19:03:09 +0000 (19:03 +0000)]
bug fixing ...

8 years agoinitial support for lfpx (replaces lpx and the parked llpx)
Ferruccio Guidi [Tue, 24 May 2016 18:59:39 +0000 (18:59 +0000)]
initial support for lfpx (replaces lpx and the parked llpx)

8 years agoadded config.ac to the tarball for debian packages
Claudio Sacerdoti Coen [Tue, 24 May 2016 09:24:59 +0000 (09:24 +0000)]
added config.ac to the tarball for debian packages

Was it really required? I don't know but it worked like that before.

8 years agoinitial support for LaTeX-defined notatopn
Ferruccio Guidi [Mon, 23 May 2016 20:27:38 +0000 (20:27 +0000)]
initial support for LaTeX-defined notatopn

8 years ago- support fof global alpha-conversion with hyperlinks
Ferruccio Guidi [Sun, 22 May 2016 20:00:11 +0000 (20:00 +0000)]
- support fof global alpha-conversion with hyperlinks
- Makefile: a bug fixed

8 years agoupdate in basic_2
Ferruccio Guidi [Sun, 22 May 2016 13:26:00 +0000 (13:26 +0000)]
update in basic_2

8 years ago- notational change for cpg and cpx
Ferruccio Guidi [Sun, 22 May 2016 11:28:36 +0000 (11:28 +0000)]
- notational change for cpg and cpx
- versions table updated on site

8 years agoupdate in basic_2
Ferruccio Guidi [Sat, 21 May 2016 20:23:20 +0000 (20:23 +0000)]
update in basic_2

8 years ago- first results on cpx (dericed from those on cpg)
Ferruccio Guidi [Sat, 21 May 2016 20:21:35 +0000 (20:21 +0000)]
- first results on cpx (dericed from those on cpg)
- minor bugs fixed

8 years agoupdate in ground_2 and basic_2
Ferruccio Guidi [Thu, 19 May 2016 10:18:31 +0000 (10:18 +0000)]
update in ground_2 and basic_2

8 years agobug fix in cpg allows to prove lsubr_cpg_trans
Ferruccio Guidi [Thu, 19 May 2016 10:16:22 +0000 (10:16 +0000)]
bug fix in cpg allows to prove lsubr_cpg_trans

8 years ago- ground_2: support for lifts_div4
Ferruccio Guidi [Wed, 18 May 2016 18:44:46 +0000 (18:44 +0000)]
- ground_2: support for lifts_div4
- basic_2: cpg_drops competed

8 years agonews for matita 0.99.3
Ferruccio Guidi [Wed, 18 May 2016 15:59:51 +0000 (15:59 +0000)]
news for matita 0.99.3

8 years agothe source code of matita 0.99.3 is online
Ferruccio Guidi [Wed, 18 May 2016 15:36:43 +0000 (15:36 +0000)]
the source code of matita 0.99.3 is online

8 years agobugfix ind docbook code for the relise of matita 0.99.3
Ferruccio Guidi [Wed, 18 May 2016 15:35:39 +0000 (15:35 +0000)]
bugfix ind docbook code for the relise of matita 0.99.3

8 years agosome renaming and reordering of variables
Ferruccio Guidi [Sun, 8 May 2016 18:56:11 +0000 (18:56 +0000)]
some renaming and reordering of variables
the commit works up tp the "static" component + lpg.ma

8 years agopre commit for matita version 0.99.3
Ferruccio Guidi [Fri, 6 May 2016 15:37:58 +0000 (15:37 +0000)]
pre commit for matita version 0.99.3

8 years ago- matex: support for alpha-conversion completed
Ferruccio Guidi [Sat, 30 Apr 2016 21:33:47 +0000 (21:33 +0000)]
- matex: support for alpha-conversion completed
- matex.sty: hyperlinks without labels
- registry: support or triples

8 years agoexportation of lambdadelta 1 with flavoured let recs
Ferruccio Guidi [Wed, 27 Apr 2016 16:25:05 +0000 (16:25 +0000)]
exportation of lambdadelta 1 with flavoured let recs

8 years ago- partial commit of rt_transition ...
Ferruccio Guidi [Fri, 22 Apr 2016 14:23:31 +0000 (14:23 +0000)]
- partial commit of rt_transition  ...
- renaming in equivalence, dynamic, examples

8 years agomilestone in basic_2 ...
Ferruccio Guidi [Mon, 18 Apr 2016 18:36:29 +0000 (18:36 +0000)]
milestone in basic_2 ...

8 years agoground_2: generic rt-transition counter
Ferruccio Guidi [Mon, 18 Apr 2016 18:30:57 +0000 (18:30 +0000)]
ground_2: generic rt-transition counter

8 years agoAs required by M. Maietti,
Ferruccio Guidi [Mon, 18 Apr 2016 15:29:33 +0000 (15:29 +0000)]
As required by M. Maietti,
cyclic sort hierarchies are now allowed through the "cyclic" keyword
so we can write:
universe cyclic constraint Type[U] < Type[U].
definition inconsistent: Type[U] ≝ Type[U].
matitaclean all is required after this commit

8 years agorefactoring to park the notions:
Ferruccio Guidi [Sat, 16 Apr 2016 22:01:54 +0000 (22:01 +0000)]
refactoring to park the notions:
lstas, unfold, crr, cir, cnr, crx, cix, cnx

8 years agouniversary milestone in basic_2
Ferruccio Guidi [Sat, 16 Apr 2016 12:53:51 +0000 (12:53 +0000)]
universary milestone in basic_2

8 years ago- former llpx_sn an lleq reactivated as lfxs and lfeq
Ferruccio Guidi [Sat, 16 Apr 2016 12:43:32 +0000 (12:43 +0000)]
- former llpx_sn an lleq reactivated as lfxs and lfeq

8 years ago- first working commit of the static component ..
Ferruccio Guidi [Tue, 12 Apr 2016 14:27:22 +0000 (14:27 +0000)]
- first working commit of the static component ..
- updates on some web pages

8 years ago- advances on drops
Ferruccio Guidi [Mon, 11 Apr 2016 17:15:40 +0000 (17:15 +0000)]
- advances on drops
- partial commit of the "static" component

8 years agorenaming ...
Ferruccio Guidi [Fri, 8 Apr 2016 21:34:02 +0000 (21:34 +0000)]
renaming ...

8 years agominor additions :)
Ferruccio Guidi [Fri, 8 Apr 2016 21:30:19 +0000 (21:30 +0000)]
minor additions :)

8 years agoupdate in ground_2 and basic_2
Ferruccio Guidi [Fri, 8 Apr 2016 20:52:38 +0000 (20:52 +0000)]
update in ground_2 and basic_2

8 years ago- commit of the "s_computation" component ...
Ferruccio Guidi [Fri, 8 Apr 2016 20:49:11 +0000 (20:49 +0000)]
- commit of the "s_computation" component ...
- additions in ground_2/relocation
- milestonee added in basic_2
- minor corrections

8 years agothe newly generated web pages ...
Ferruccio Guidi [Thu, 7 Apr 2016 13:50:13 +0000 (13:50 +0000)]
the newly generated web pages ...

8 years ago- advances in the site generation architecture
Ferruccio Guidi [Thu, 7 Apr 2016 13:34:39 +0000 (13:34 +0000)]
- advances in the site generation architecture
- more on OSN and on the disclaimer

8 years agoone file was missing
Ferruccio Guidi [Mon, 4 Apr 2016 22:17:16 +0000 (22:17 +0000)]
one file was missing

8 years agoEBNF definition of OSN begins ...
Ferruccio Guidi [Mon, 4 Apr 2016 22:16:36 +0000 (22:16 +0000)]
EBNF definition of OSN begins ...

8 years ago- initial description of OSN
Ferruccio Guidi [Sun, 3 Apr 2016 20:52:04 +0000 (20:52 +0000)]
- initial description of OSN
- ld_web: minor updates

8 years agoimages for Open Symbolic Notation (OSN)
Ferruccio Guidi [Sun, 3 Apr 2016 13:10:21 +0000 (13:10 +0000)]
images for Open Symbolic Notation (OSN)

8 years agoupdate in ground_2 and basic_2 ...
Ferruccio Guidi [Fri, 1 Apr 2016 21:31:50 +0000 (21:31 +0000)]
update in ground_2 and basic_2 ...

8 years ago- new component "s_transition" for the restored fqu and fquq
Ferruccio Guidi [Fri, 1 Apr 2016 21:26:20 +0000 (21:26 +0000)]
- new component "s_transition" for the restored fqu and fquq
- minor additions
- notation update
- partial commit in the "static" component to park da and lsubd

8 years ago- uniform relocations
Ferruccio Guidi [Thu, 31 Mar 2016 14:44:31 +0000 (14:44 +0000)]
- uniform relocations
- more results on at and after

8 years agominor correction on "source" production
Ferruccio Guidi [Mon, 28 Mar 2016 16:27:25 +0000 (16:27 +0000)]
minor correction on "source" production

8 years agominor additions ...
Ferruccio Guidi [Mon, 28 Mar 2016 16:04:59 +0000 (16:04 +0000)]
minor additions ...

8 years agoupdate in basic_2 and apps_2 ...
Ferruccio Guidi [Sun, 27 Mar 2016 16:43:13 +0000 (16:43 +0000)]
update in basic_2 and apps_2 ...

8 years ago- minor corrections
Ferruccio Guidi [Sun, 27 Mar 2016 16:39:33 +0000 (16:39 +0000)]
- minor corrections
- web pages for nasoc_2 and apps_2 are up again

8 years agoanother file was missing :(
Ferruccio Guidi [Fri, 25 Mar 2016 20:06:48 +0000 (20:06 +0000)]
another file was missing :(

8 years ago- probe: now includes source character count (was: mac)
Ferruccio Guidi [Fri, 25 Mar 2016 18:48:24 +0000 (18:48 +0000)]
- probe: now includes source character count (was: mac)
- lambdadelta: summaries are generated using the updated probe

8 years agosupport for printing the number of objects grouped by flavour
Ferruccio Guidi [Thu, 24 Mar 2016 12:23:19 +0000 (12:23 +0000)]
support for printing the number of objects grouped by flavour

8 years agomore files to commit .... :(
Ferruccio Guidi [Wed, 23 Mar 2016 19:13:00 +0000 (19:13 +0000)]
more files to commit .... :(

8 years ago- ng_kernel: we print the offending term when guarded_by_constructors fails
Ferruccio Guidi [Wed, 23 Mar 2016 19:10:29 +0000 (19:10 +0000)]
- ng_kernel: we print the offending term when guarded_by_constructors fails
- probe: we print the roots when more than one root is found
- lambdadelta: first working commit for the "relocation" component

8 years agoupdate in ground_2
Ferruccio Guidi [Mon, 21 Mar 2016 19:39:42 +0000 (19:39 +0000)]
update in ground_2

8 years agortmaps with finite colength
Ferruccio Guidi [Mon, 21 Mar 2016 19:36:29 +0000 (19:36 +0000)]
rtmaps with finite colength

8 years agoadvances in the theory of drops, lexs, and frees ...
Ferruccio Guidi [Fri, 18 Mar 2016 14:25:19 +0000 (14:25 +0000)]
advances in the theory of drops, lexs, and frees ...

8 years ago- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)
Ferruccio Guidi [Sun, 13 Mar 2016 17:30:14 +0000 (17:30 +0000)]
- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)
- source specifier on inductive/coinductive types (implies matitaclan all)
- minor additions

8 years ago- ground_2: some additions
Ferruccio Guidi [Thu, 10 Mar 2016 21:16:20 +0000 (21:16 +0000)]
- ground_2: some additions
- basic_2/grammar: added missing files

8 years agopartial commit in the relocation component to move some files ...
Ferruccio Guidi [Thu, 10 Mar 2016 21:12:43 +0000 (21:12 +0000)]
partial commit in the relocation component to move some files ...

8 years agomore results on after ...
Ferruccio Guidi [Mon, 7 Mar 2016 17:04:28 +0000 (17:04 +0000)]
more results on after ...

8 years agosmall improvements and corrections ...
Ferruccio Guidi [Fri, 4 Mar 2016 19:52:33 +0000 (19:52 +0000)]
small improvements and corrections ...

8 years agosome corrections ...
Ferruccio Guidi [Fri, 4 Mar 2016 19:51:20 +0000 (19:51 +0000)]
some corrections ...

8 years agomailstone in ground_2 ...
Ferruccio Guidi [Fri, 4 Mar 2016 15:18:05 +0000 (15:18 +0000)]
mailstone in ground_2 ...

8 years agocommitcompleted: some files were missing :(
Ferruccio Guidi [Fri, 4 Mar 2016 15:14:13 +0000 (15:14 +0000)]
commitcompleted: some files were missing :(

8 years agortmap (platform-indepent multple relocation): application and composition
Ferruccio Guidi [Fri, 4 Mar 2016 13:39:02 +0000 (13:39 +0000)]
rtmap (platform-indepent multple relocation): application and composition

8 years ago- second precommit for rtmap
Ferruccio Guidi [Wed, 2 Mar 2016 21:32:00 +0000 (21:32 +0000)]
- second precommit for rtmap
- we park relocation by streams of booleans

8 years agoprecommit for rtmap ...
Ferruccio Guidi [Tue, 23 Feb 2016 15:36:51 +0000 (15:36 +0000)]
precommit for rtmap ...

8 years agoMaTeX
Ferruccio Guidi [Sun, 21 Feb 2016 15:30:59 +0000 (15:30 +0000)]
MaTeX
- bug fixed in rendering of application: the head was not rendered sometimes
- we can generate the list of the produced TeX files
- TeX item for comments was missing
test
- bug fixed in matex.sty: pages were not ejected properly causig memory overflow
- now includes the whole \lambda\delta version 1 (737 pages for now)
- object numbering is now supported

8 years agonow every object is output in a LaTeX environment, not just proofs
Ferruccio Guidi [Mon, 15 Feb 2016 21:29:10 +0000 (21:29 +0000)]
now every object is output in a LaTeX environment, not just proofs

8 years agofirst commit for lreq ...
Ferruccio Guidi [Wed, 10 Feb 2016 19:02:11 +0000 (19:02 +0000)]
first commit for lreq ...

8 years ago- ground_2: update ...
Ferruccio Guidi [Wed, 10 Feb 2016 12:03:01 +0000 (12:03 +0000)]
- ground_2: update ...
- basic_2: first commit for lexs ...

8 years agopre commit for lexs ...
Ferruccio Guidi [Wed, 10 Feb 2016 11:20:14 +0000 (11:20 +0000)]
pre commit for lexs ...

8 years agogeneral slicing reactivated ...
Ferruccio Guidi [Tue, 9 Feb 2016 19:05:48 +0000 (19:05 +0000)]
general slicing reactivated ...

8 years agoupdate in ground_2
Ferruccio Guidi [Sun, 7 Feb 2016 17:55:13 +0000 (17:55 +0000)]
update in ground_2

8 years ago- ground_2: support for relocation updated
Ferruccio Guidi [Sun, 7 Feb 2016 17:45:09 +0000 (17:45 +0000)]
- ground_2: support for relocation updated
- basic_2: theory of relocation updated
- MaTeX: (co)inductive types are now processed

8 years ago- ground_2: relocation with nstream is now based on two basic functions (push and...
Ferruccio Guidi [Thu, 4 Feb 2016 15:35:23 +0000 (15:35 +0000)]
- ground_2: relocation with nstream is now based on two basic functions (push and next)
- matex: scope management completed! stylesheet improved (also with colors)

8 years ago- scope management completed
Ferruccio Guidi [Tue, 2 Feb 2016 16:52:55 +0000 (16:52 +0000)]
- scope management completed
- improved style sheet and test document

8 years ago- scope management begins...
Ferruccio Guidi [Tue, 2 Feb 2016 00:00:19 +0000 (00:00 +0000)]
- scope management begins...
- improved style sheet

8 years agoimproved style sheet
Ferruccio Guidi [Mon, 1 Feb 2016 00:20:16 +0000 (00:20 +0000)]
improved style sheet

8 years agorenaming ...
Ferruccio Guidi [Sun, 31 Jan 2016 14:37:43 +0000 (14:37 +0000)]
renaming ...

8 years agosome renaming ...
Ferruccio Guidi [Sat, 30 Jan 2016 14:10:38 +0000 (14:10 +0000)]
some renaming ...

8 years agolift functions and identity map
Ferruccio Guidi [Fri, 29 Jan 2016 14:48:27 +0000 (14:48 +0000)]
lift functions and identity map

8 years agolexicon commands must tbe parsed before grafite commands rather than
Ferruccio Guidi [Tue, 26 Jan 2016 16:09:51 +0000 (16:09 +0000)]
lexicon commands must tbe parsed before grafite commands rather than
after (why?)

8 years agodocumentation update
Ferruccio Guidi [Sat, 23 Jan 2016 08:51:34 +0000 (08:51 +0000)]
documentation update

8 years agonstream: composition completed :)
Ferruccio Guidi [Wed, 20 Jan 2016 21:37:35 +0000 (21:37 +0000)]
nstream: composition completed :)

8 years agoground_2: web page update
Ferruccio Guidi [Thu, 14 Jan 2016 22:19:57 +0000 (22:19 +0000)]
ground_2: web page update

8 years agomissing notation file
Ferruccio Guidi [Wed, 13 Jan 2016 20:35:12 +0000 (20:35 +0000)]
missing notation file

8 years ago- ng_kernel: catched Invalid_argument "List.nth" in typeof of Rel i (raied when i...
Ferruccio Guidi [Wed, 13 Jan 2016 20:33:18 +0000 (20:33 +0000)]
- ng_kernel: catched Invalid_argument "List.nth" in typeof of Rel i (raied when i < 1)
- ground_1: relocation with streams of natural numbers begins

8 years ago- plain anticipation for CIC proofs terms
Ferruccio Guidi [Mon, 11 Jan 2016 16:46:16 +0000 (16:46 +0000)]
- plain anticipation for CIC proofs terms
- support for (co)fixpoint objects
- Makefile for testing
- minor updates

8 years ago- Const is now processed properly
Ferruccio Guidi [Mon, 4 Jan 2016 12:33:52 +0000 (12:33 +0000)]
- Const is now processed properly

8 years agomore minor bugs fixed in the web site
Ferruccio Guidi [Wed, 30 Dec 2015 14:35:04 +0000 (14:35 +0000)]
more minor bugs fixed in the web site

8 years agominor bugs fixed in the web site, and minor updates
Ferruccio Guidi [Wed, 30 Dec 2015 14:06:17 +0000 (14:06 +0000)]
minor bugs fixed in the web site, and minor updates

8 years agosite update for helena 0.8.3
Ferruccio Guidi [Wed, 30 Dec 2015 12:02:25 +0000 (12:02 +0000)]
site update for helena 0.8.3