]>
matita.cs.unibo.it Git - helm.git/log
Ferruccio Guidi [Fri, 1 Jul 2016 13:59:41 +0000 (13:59 +0000)]
first definition of cpm:
the contextual rule for cast is incorrect :(
Ferruccio Guidi [Mon, 27 Jun 2016 18:57:09 +0000 (18:57 +0000)]
update in basic_2 ...
Ferruccio Guidi [Mon, 27 Jun 2016 18:54:28 +0000 (18:54 +0000)]
lfpx_drops completed!
Ferruccio Guidi [Sat, 25 Jun 2016 17:52:28 +0000 (17:52 +0000)]
totality of co-composition !
Ferruccio Guidi [Fri, 24 Jun 2016 13:41:09 +0000 (13:41 +0000)]
more notation for basic_1 ...
Ferruccio Guidi [Wed, 22 Jun 2016 19:46:32 +0000 (19:46 +0000)]
- matex: minor improvements
- latex stylesheets: more notation for basic_1
now we use just the stix fonts
Ferruccio Guidi [Mon, 20 Jun 2016 21:39:29 +0000 (21:39 +0000)]
updating the dropable-related definitions with coafter ...
Ferruccio Guidi [Mon, 20 Jun 2016 18:54:46 +0000 (18:54 +0000)]
corrections to use less font packages (TeX was complaining)
Ferruccio Guidi [Sun, 19 Jun 2016 12:59:00 +0000 (12:59 +0000)]
- matex: minor corrections to handle applications with many arguments
- matex test stylesheets: some improvements, notation for ground_1 completed
Ferruccio Guidi [Mon, 13 Jun 2016 16:27:50 +0000 (16:27 +0000)]
does_not_occur documented
Ferruccio Guidi [Sun, 12 Jun 2016 17:36:44 +0000 (17:36 +0000)]
- improved support for case
- support for renaming constants
Ferruccio Guidi [Thu, 9 Jun 2016 14:47:29 +0000 (14:47 +0000)]
update in ground_2 and basic_2
Ferruccio Guidi [Thu, 9 Jun 2016 14:45:23 +0000 (14:45 +0000)]
frees_drops completed!
Ferruccio Guidi [Mon, 6 Jun 2016 20:20:44 +0000 (20:20 +0000)]
work in progress on frees_drops
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
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
Ferruccio Guidi [Tue, 31 May 2016 19:19:40 +0000 (19:19 +0000)]
- update in ground_2 and basic_2
- updated documentation
Ferruccio Guidi [Tue, 31 May 2016 19:06:53 +0000 (19:06 +0000)]
frees_drops, initial versrion
Ferruccio Guidi [Mon, 30 May 2016 18:57:34 +0000 (18:57 +0000)]
some results on co-composition ...
Ferruccio Guidi [Sun, 29 May 2016 18:13:10 +0000 (18:13 +0000)]
more results on sor ...
Ferruccio Guidi [Wed, 25 May 2016 12:12:25 +0000 (12:12 +0000)]
initial support for lfpx_drops ...
Ferruccio Guidi [Tue, 24 May 2016 19:05:12 +0000 (19:05 +0000)]
more files missing :((
Ferruccio Guidi [Tue, 24 May 2016 19:04:08 +0000 (19:04 +0000)]
une file was missing :(
Ferruccio Guidi [Tue, 24 May 2016 19:03:09 +0000 (19:03 +0000)]
bug fixing ...
Ferruccio Guidi [Tue, 24 May 2016 18:59:39 +0000 (18:59 +0000)]
initial support for lfpx (replaces lpx and the parked llpx)
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.
Ferruccio Guidi [Mon, 23 May 2016 20:27:38 +0000 (20:27 +0000)]
initial support for LaTeX-defined notatopn
Ferruccio Guidi [Sun, 22 May 2016 20:00:11 +0000 (20:00 +0000)]
- support fof global alpha-conversion with hyperlinks
- Makefile: a bug fixed
Ferruccio Guidi [Sun, 22 May 2016 13:26:00 +0000 (13:26 +0000)]
update in basic_2
Ferruccio Guidi [Sun, 22 May 2016 11:28:36 +0000 (11:28 +0000)]
- notational change for cpg and cpx
- versions table updated on site
Ferruccio Guidi [Sat, 21 May 2016 20:23:20 +0000 (20:23 +0000)]
update in basic_2
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
Ferruccio Guidi [Thu, 19 May 2016 10:18:31 +0000 (10:18 +0000)]
update in ground_2 and basic_2
Ferruccio Guidi [Thu, 19 May 2016 10:16:22 +0000 (10:16 +0000)]
bug fix in cpg allows to prove lsubr_cpg_trans
Ferruccio Guidi [Wed, 18 May 2016 18:44:46 +0000 (18:44 +0000)]
- ground_2: support for lifts_div4
- basic_2: cpg_drops competed
Ferruccio Guidi [Wed, 18 May 2016 15:59:51 +0000 (15:59 +0000)]
news for matita 0.99.3
Ferruccio Guidi [Wed, 18 May 2016 15:36:43 +0000 (15:36 +0000)]
the source code of matita 0.99.3 is online
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
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
Ferruccio Guidi [Fri, 6 May 2016 15:37:58 +0000 (15:37 +0000)]
pre commit for matita version 0.99.3
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
Ferruccio Guidi [Wed, 27 Apr 2016 16:25:05 +0000 (16:25 +0000)]
exportation of lambdadelta 1 with flavoured let recs
Ferruccio Guidi [Fri, 22 Apr 2016 14:23:31 +0000 (14:23 +0000)]
- partial commit of rt_transition ...
- renaming in equivalence, dynamic, examples
Ferruccio Guidi [Mon, 18 Apr 2016 18:36:29 +0000 (18:36 +0000)]
milestone in basic_2 ...
Ferruccio Guidi [Mon, 18 Apr 2016 18:30:57 +0000 (18:30 +0000)]
ground_2: generic rt-transition counter
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
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
Ferruccio Guidi [Sat, 16 Apr 2016 12:53:51 +0000 (12:53 +0000)]
universary milestone in basic_2
Ferruccio Guidi [Sat, 16 Apr 2016 12:43:32 +0000 (12:43 +0000)]
- former llpx_sn an lleq reactivated as lfxs and lfeq
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
Ferruccio Guidi [Mon, 11 Apr 2016 17:15:40 +0000 (17:15 +0000)]
- advances on drops
- partial commit of the "static" component
Ferruccio Guidi [Fri, 8 Apr 2016 21:34:02 +0000 (21:34 +0000)]
renaming ...
Ferruccio Guidi [Fri, 8 Apr 2016 21:30:19 +0000 (21:30 +0000)]
minor additions :)
Ferruccio Guidi [Fri, 8 Apr 2016 20:52:38 +0000 (20:52 +0000)]
update in ground_2 and basic_2
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
Ferruccio Guidi [Thu, 7 Apr 2016 13:50:13 +0000 (13:50 +0000)]
the newly generated web pages ...
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
Ferruccio Guidi [Mon, 4 Apr 2016 22:17:16 +0000 (22:17 +0000)]
one file was missing
Ferruccio Guidi [Mon, 4 Apr 2016 22:16:36 +0000 (22:16 +0000)]
EBNF definition of OSN begins ...
Ferruccio Guidi [Sun, 3 Apr 2016 20:52:04 +0000 (20:52 +0000)]
- initial description of OSN
- ld_web: minor updates
Ferruccio Guidi [Sun, 3 Apr 2016 13:10:21 +0000 (13:10 +0000)]
images for Open Symbolic Notation (OSN)
Ferruccio Guidi [Fri, 1 Apr 2016 21:31:50 +0000 (21:31 +0000)]
update in ground_2 and basic_2 ...
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
Ferruccio Guidi [Thu, 31 Mar 2016 14:44:31 +0000 (14:44 +0000)]
- uniform relocations
- more results on at and after
Ferruccio Guidi [Mon, 28 Mar 2016 16:27:25 +0000 (16:27 +0000)]
minor correction on "source" production
Ferruccio Guidi [Mon, 28 Mar 2016 16:04:59 +0000 (16:04 +0000)]
minor additions ...
Ferruccio Guidi [Sun, 27 Mar 2016 16:43:13 +0000 (16:43 +0000)]
update in basic_2 and apps_2 ...
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
Ferruccio Guidi [Fri, 25 Mar 2016 20:06:48 +0000 (20:06 +0000)]
another file was missing :(
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
Ferruccio Guidi [Thu, 24 Mar 2016 12:23:19 +0000 (12:23 +0000)]
support for printing the number of objects grouped by flavour
Ferruccio Guidi [Wed, 23 Mar 2016 19:13:00 +0000 (19:13 +0000)]
more files to commit .... :(
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
Ferruccio Guidi [Mon, 21 Mar 2016 19:39:42 +0000 (19:39 +0000)]
update in ground_2
Ferruccio Guidi [Mon, 21 Mar 2016 19:36:29 +0000 (19:36 +0000)]
rtmaps with finite colength
Ferruccio Guidi [Fri, 18 Mar 2016 14:25:19 +0000 (14:25 +0000)]
advances in the theory of drops, lexs, and frees ...
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
Ferruccio Guidi [Thu, 10 Mar 2016 21:16:20 +0000 (21:16 +0000)]
- ground_2: some additions
- basic_2/grammar: added missing files
Ferruccio Guidi [Thu, 10 Mar 2016 21:12:43 +0000 (21:12 +0000)]
partial commit in the relocation component to move some files ...
Ferruccio Guidi [Mon, 7 Mar 2016 17:04:28 +0000 (17:04 +0000)]
more results on after ...
Ferruccio Guidi [Fri, 4 Mar 2016 19:52:33 +0000 (19:52 +0000)]
small improvements and corrections ...
Ferruccio Guidi [Fri, 4 Mar 2016 19:51:20 +0000 (19:51 +0000)]
some corrections ...
Ferruccio Guidi [Fri, 4 Mar 2016 15:18:05 +0000 (15:18 +0000)]
mailstone in ground_2 ...
Ferruccio Guidi [Fri, 4 Mar 2016 15:14:13 +0000 (15:14 +0000)]
commitcompleted: some files were missing :(
Ferruccio Guidi [Fri, 4 Mar 2016 13:39:02 +0000 (13:39 +0000)]
rtmap (platform-indepent multple relocation): application and composition
Ferruccio Guidi [Wed, 2 Mar 2016 21:32:00 +0000 (21:32 +0000)]
- second precommit for rtmap
- we park relocation by streams of booleans
Ferruccio Guidi [Tue, 23 Feb 2016 15:36:51 +0000 (15:36 +0000)]
precommit for rtmap ...
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
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
Ferruccio Guidi [Wed, 10 Feb 2016 19:02:11 +0000 (19:02 +0000)]
first commit for lreq ...
Ferruccio Guidi [Wed, 10 Feb 2016 12:03:01 +0000 (12:03 +0000)]
- ground_2: update ...
- basic_2: first commit for lexs ...
Ferruccio Guidi [Wed, 10 Feb 2016 11:20:14 +0000 (11:20 +0000)]
pre commit for lexs ...
Ferruccio Guidi [Tue, 9 Feb 2016 19:05:48 +0000 (19:05 +0000)]
general slicing reactivated ...
Ferruccio Guidi [Sun, 7 Feb 2016 17:55:13 +0000 (17:55 +0000)]
update in ground_2
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
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)
Ferruccio Guidi [Tue, 2 Feb 2016 16:52:55 +0000 (16:52 +0000)]
- scope management completed
- improved style sheet and test document
Ferruccio Guidi [Tue, 2 Feb 2016 00:00:19 +0000 (00:00 +0000)]
- scope management begins...
- improved style sheet
Ferruccio Guidi [Mon, 1 Feb 2016 00:20:16 +0000 (00:20 +0000)]
improved style sheet
Ferruccio Guidi [Sun, 31 Jan 2016 14:37:43 +0000 (14:37 +0000)]
renaming ...