]>
matita.cs.unibo.it Git - helm.git/log
Andrea Berlingieri [Thu, 14 Mar 2019 09:31:01 +0000 (10:31 +0100)]
Partially restore the suppose tactic
Add a type for the suppose tactic in GrafiteAst
Add pretty printing code for the suppose tactic
Add a parsing rule for the suppose tactic in GrafiteParser
Add a call in to the suppose tactic in GrafiteEngine
Add code for the suppose tactic in Declarative
Add syntax highlight tag for the suppose tactic
Andrea Berlingieri [Wed, 13 Mar 2019 22:18:13 +0000 (23:18 +0100)]
Partially restore the assume tactic
Add a type for the assume tactic in GrafiteAst
Add pretty printing code for the assume tactic
Add a parsing rule for the assume tactic in GrafiteParser
Add a call in to the assume tactic in GrafiteEngine
Add a file for the declarative tactics to the ng_tactics module
Add code for the assume tactic in Declarative
Add syntax highlight tag for the assume tactic
Add the exact_tac signature to the interface file of nTactics
Claudio Sacerdoti Coen [Fri, 27 Sep 2019 13:55:14 +0000 (15:55 +0200)]
porting to recent ocaml
Claudio Sacerdoti Coen [Fri, 27 Sep 2019 13:54:23 +0000 (15:54 +0200)]
...
Claudio Sacerdoti Coen [Fri, 27 Sep 2019 13:51:52 +0000 (15:51 +0200)]
lablgtk3.sourceview3 => lablgtk3-sourceview3
Ferruccio Guidi [Tue, 8 Jan 2019 15:34:20 +0000 (16:34 +0100)]
patches for compilation with ocaml 4.0.5
+ lambdadelta website update
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 15:31:45 +0000 (16:31 +0100)]
finite_lambda restored
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 15:25:21 +0000 (16:25 +0100)]
reverse_complexity lib restored
the toolkit.ma file contains errors. I have
commented out a few places
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 14:33:07 +0000 (15:33 +0100)]
make depend.opt
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 13:02:54 +0000 (14:02 +0100)]
make dist repaired
- svn export => git archive
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 12:52:04 +0000 (13:52 +0100)]
version upgrade
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 00:25:46 +0000 (01:25 +0100)]
added missing libs detection
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 00:19:15 +0000 (01:19 +0100)]
Most warnings turned into errors and avoided
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 21:17:21 +0000 (22:17 +0100)]
0.99.3 -> 0.99.4
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 21:01:16 +0000 (22:01 +0100)]
report_error dialog ported to gtk3
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 20:46:50 +0000 (21:46 +0100)]
Quit without saving dialog fixed
Ported to gtk3
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:40:44 +0000 (19:40 +0100)]
useful comment
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:20:21 +0000 (19:20 +0100)]
automatically inserted aliases
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:18:24 +0000 (19:18 +0100)]
Matita 0.99.* bug fixed: new alias insertion
Fixed a bug that was there since the new Matita
generation: new_aliases were always computed
as empty and thus never inserted.
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 16:03:07 +0000 (17:03 +0100)]
use #run for dialog
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:38:07 +0000 (16:38 +0100)]
Let the widget expand in the old way
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:11:24 +0000 (16:11 +0100)]
Old glade2 file removed
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:09:34 +0000 (16:09 +0100)]
Broken libs moved to broken_lib
Some can probably be restored with some love.
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 12:38:12 +0000 (13:38 +0100)]
lablgladecc => lablgladecc3
It now compiles with lablgtk3 opam package
Claudio Sacerdoti Coen [Mon, 24 Dec 2018 00:05:41 +0000 (01:05 +0100)]
disambiguationErrors now uses #run
correct Gtk behavior
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 14:32:24 +0000 (15:32 +0100)]
code for DisambiguationErrors simplified
Still not working (since matita 0.99x?)
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:19:30 +0000 (01:19 +0100)]
several dialog boxes no longer used removed
they were dead code in current Matita
I only left the AutoWin and the ones used
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:12:51 +0000 (01:12 +0100)]
last deprecated widget updated
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:09:10 +0000 (01:09 +0100)]
findReplace ported from GtkTable to GtkGrid
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:42:49 +0000 (00:42 +0100)]
More H/V deprecated widgets replaced
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:39:03 +0000 (00:39 +0100)]
GtkHSeparator deprecated
GtkSeparator used instead
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:35:11 +0000 (00:35 +0100)]
HandleBox deprecated and no longer working
Replace with Box. It is used for natural
deduction palette that is not very useful
yet in the new Matita.
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:06:14 +0000 (00:06 +0100)]
comment
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:05:24 +0000 (00:05 +0100)]
Fixes to show coercion graph
- new bug in dot avoided (graphviz commands
no longer chainable)
- avoided bug that printed a broken icon in
place of an empty graph; now we print
nothing (a cleared pixbuf) which is not
white. It would be better to show
something to make clear the graph is empty
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 20:47:51 +0000 (21:47 +0100)]
Fix dialog win
It used to be destroyed when closed the first time
Claudio Sacerdoti Coen [Thu, 20 Dec 2018 22:12:36 +0000 (23:12 +0100)]
Use lablgladecc -embed again
Claudio Sacerdoti Coen [Fri, 14 Dec 2018 23:15:58 +0000 (00:15 +0100)]
On-going porting to lablgtk3
Ferruccio Guidi [Mon, 23 Sep 2019 13:00:45 +0000 (15:00 +0200)]
update in basic_2
+ main result on acle proved
Ferruccio Guidi [Wed, 18 Sep 2019 16:39:16 +0000 (18:39 +0200)]
update in static_2
+ preorder on applicability domains
+ minor bug fixes
Ferruccio Guidi [Wed, 18 Sep 2019 16:36:13 +0000 (18:36 +0200)]
new web site page
change log for λδ begins
Ferruccio Guidi [Wed, 18 Sep 2019 16:30:22 +0000 (18:30 +0200)]
update in static_2 and basic_2
+ advances on ntas for the article
+ minor corrections
+ notation update for: ac, cnv, lsubv, nta, ntas
+ bold digits in predefined virtuals
Ferruccio Guidi [Tue, 3 Sep 2019 17:36:47 +0000 (19:36 +0200)]
milestone in basic_2
We parametrize applicability condition with a generic subset of numbers.
Ferruccio Guidi [Sat, 31 Aug 2019 20:01:18 +0000 (22:01 +0200)]
update in static_2 and basic_2
+ a weaker version of tueq reintroduced
+ some renaming
+ one conjecture to prove
Ferruccio Guidi [Fri, 23 Aug 2019 19:24:02 +0000 (21:24 +0200)]
update in ground_2 static_2 basic_2
+ the applicability parameter is now a predicate
+ tueq removed in favor of theq
+ two conjectures to prove ...
Ferruccio Guidi [Mon, 19 Aug 2019 21:31:18 +0000 (23:31 +0200)]
still more additions and corrections for the article
+ one theorem was missing
+ some renaming
Ferruccio Guidi [Fri, 26 Jul 2019 14:52:57 +0000 (16:52 +0200)]
still more additions and corrections for the article
+ new proof of csx_rsx
+ more results on jsx
+ extra parameter removed from jsx
+ minor corrections on lsubr
+ some renaming
Ferruccio Guidi [Sat, 20 Jul 2019 20:13:45 +0000 (22:13 +0200)]
more additions and corrections for the article
+ fqu_clear excluded from (fqu true)
+ some renaming and changes of notation (esp. lsubsx)
+ more comments and additions to etc
+ matitadep: -b show the recursive backward dependences of a file
Ferruccio Guidi [Mon, 15 Jul 2019 17:40:22 +0000 (19:40 +0200)]
additions and corrections for the article on λδ-2B
+ candidates: condition S4 removed
+ arity assignment: decidability proved
+ minor additions
Ferruccio Guidi [Sat, 15 Jun 2019 13:19:59 +0000 (15:19 +0200)]
updating the structures for sorts
+ strict monotonicity is now an optional property
+ new optional properties: acyclicity and decidability
+ "next" now has a specific notation
+ refactored sort degree is now based on acyclicity and decidability
Ferruccio Guidi [Thu, 13 Jun 2019 15:07:51 +0000 (17:07 +0200)]
some restyling ...
+ fixing some notations
+ fixing some spaces
Ferruccio Guidi [Sun, 2 Jun 2019 13:52:42 +0000 (15:52 +0200)]
milestone in basic_2
+ Parametrized applicability condition allows λδ-2B to generalize both λδ-1A and λδ-1B.
+ ground_2: minor additions
Ferruccio Guidi [Thu, 30 May 2019 13:59:32 +0000 (15:59 +0200)]
update in basic_2
one file was missing in last commit :(
Ferruccio Guidi [Wed, 29 May 2019 19:52:30 +0000 (21:52 +0200)]
update in basic_2
+ totality for fixed cpce
+ Makefile: bug fixed
Ferruccio Guidi [Thu, 16 May 2019 21:55:15 +0000 (23:55 +0200)]
decentralizing core notation continues ...
+ apart, napart decentralized
Ferruccio Guidi [Wed, 17 Apr 2019 18:30:00 +0000 (20:30 +0200)]
update in basic_2
+ decidability of type inference
+ decidability of type checking
Ferruccio Guidi [Tue, 16 Apr 2019 21:11:59 +0000 (23:11 +0200)]
milestone in basic_2 with additions in static_2
+ validity is decidable
+ some renaming
+ batch compilation handles each specification separately
otherwise matitac opens too many files
Ferruccio Guidi [Mon, 8 Apr 2019 16:47:22 +0000 (18:47 +0200)]
update in basic_2
+ decidability of cpes
+ some renaming
Ferruccio Guidi [Fri, 5 Apr 2019 13:34:26 +0000 (15:34 +0200)]
update in ground_2 static_2 basic_2
structures for decidability of the validity predicate
+ cpes, cnr, cpre resumed
+ minor corrections
Ferruccio Guidi [Mon, 25 Mar 2019 16:32:22 +0000 (17:32 +0100)]
milestone in basic_2
preservation of validity for rt-computation does not need the sort degree parameter (i.e. no induction on the degree).
Ferruccio Guidi [Wed, 20 Mar 2019 11:30:38 +0000 (12:30 +0100)]
update in ground_2 static_2 basic_2
+ whd normal forms for terms with arity
+ positive abbreviations are not whd normal forms
+ minor additions
Ferruccio Guidi [Mon, 4 Mar 2019 23:35:54 +0000 (00:35 +0100)]
first steps towards decidability of the validity predicate
+ tentative definition of cwhx
Ferruccio Guidi [Mon, 4 Feb 2019 16:06:36 +0000 (17:06 +0100)]
minor corrections and updates
intensional and extensional equivalence on lists coincide
Ferruccio Guidi [Tue, 8 Jan 2019 15:34:20 +0000 (16:34 +0100)]
patches for compilation with ocaml 4.0.5
+ lambdadelta website update
Ferruccio Guidi [Tue, 1 Jan 2019 13:30:18 +0000 (14:30 +0100)]
the decentralization of core notation continues ...
subseteq notation decentralized
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 15:31:45 +0000 (16:31 +0100)]
finite_lambda restored
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 15:25:21 +0000 (16:25 +0100)]
reverse_complexity lib restored
the toolkit.ma file contains errors. I have
commented out a few places
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 14:33:07 +0000 (15:33 +0100)]
make depend.opt
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 13:02:54 +0000 (14:02 +0100)]
make dist repaired
- svn export => git archive
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 12:52:04 +0000 (13:52 +0100)]
version upgrade
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 00:25:46 +0000 (01:25 +0100)]
added missing libs detection
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 00:19:15 +0000 (01:19 +0100)]
Most warnings turned into errors and avoided
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 21:17:21 +0000 (22:17 +0100)]
0.99.3 -> 0.99.4
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 21:01:16 +0000 (22:01 +0100)]
report_error dialog ported to gtk3
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 20:46:50 +0000 (21:46 +0100)]
Quit without saving dialog fixed
Ported to gtk3
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:40:44 +0000 (19:40 +0100)]
useful comment
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:20:21 +0000 (19:20 +0100)]
automatically inserted aliases
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:18:24 +0000 (19:18 +0100)]
Matita 0.99.* bug fixed: new alias insertion
Fixed a bug that was there since the new Matita
generation: new_aliases were always computed
as empty and thus never inserted.
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 16:03:07 +0000 (17:03 +0100)]
use #run for dialog
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:38:07 +0000 (16:38 +0100)]
Let the widget expand in the old way
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:11:24 +0000 (16:11 +0100)]
Old glade2 file removed
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:09:34 +0000 (16:09 +0100)]
Broken libs moved to broken_lib
Some can probably be restored with some love.
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 12:38:12 +0000 (13:38 +0100)]
lablgladecc => lablgladecc3
It now compiles with lablgtk3 opam package
Claudio Sacerdoti Coen [Mon, 24 Dec 2018 00:05:41 +0000 (01:05 +0100)]
disambiguationErrors now uses #run
correct Gtk behavior
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 14:32:24 +0000 (15:32 +0100)]
code for DisambiguationErrors simplified
Still not working (since matita 0.99x?)
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:19:30 +0000 (01:19 +0100)]
several dialog boxes no longer used removed
they were dead code in current Matita
I only left the AutoWin and the ones used
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:12:51 +0000 (01:12 +0100)]
last deprecated widget updated
Claudio Sacerdoti Coen [Sat, 22 Dec 2018 00:09:10 +0000 (01:09 +0100)]
findReplace ported from GtkTable to GtkGrid
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:42:49 +0000 (00:42 +0100)]
More H/V deprecated widgets replaced
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:39:03 +0000 (00:39 +0100)]
GtkHSeparator deprecated
GtkSeparator used instead
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:35:11 +0000 (00:35 +0100)]
HandleBox deprecated and no longer working
Replace with Box. It is used for natural
deduction palette that is not very useful
yet in the new Matita.
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:06:14 +0000 (00:06 +0100)]
comment
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 23:05:24 +0000 (00:05 +0100)]
Fixes to show coercion graph
- new bug in dot avoided (graphviz commands
no longer chainable)
- avoided bug that printed a broken icon in
place of an empty graph; now we print
nothing (a cleared pixbuf) which is not
white. It would be better to show
something to make clear the graph is empty
Claudio Sacerdoti Coen [Fri, 21 Dec 2018 20:47:51 +0000 (21:47 +0100)]
Fix dialog win
It used to be destroyed when closed the first time
Claudio Sacerdoti Coen [Thu, 20 Dec 2018 22:12:36 +0000 (23:12 +0100)]
Use lablgladecc -embed again
Ferruccio Guidi [Thu, 20 Dec 2018 15:46:01 +0000 (16:46 +0100)]
xoa utility updated
+ two missing cases implemented
+ dependences fixed in Makefile
Claudio Sacerdoti Coen [Fri, 14 Dec 2018 23:15:58 +0000 (00:15 +0100)]
On-going porting to lablgtk3
Ferruccio Guidi [Mon, 17 Dec 2018 20:11:50 +0000 (21:11 +0100)]
list of failing files updated
+ one file added
Ferruccio Guidi [Mon, 10 Dec 2018 20:13:41 +0000 (21:13 +0100)]
web site update
one css stylesheet improved
Ferruccio Guidi [Thu, 6 Dec 2018 22:33:27 +0000 (23:33 +0100)]
web site update
+ one css file improved
Ferruccio Guidi [Sat, 1 Dec 2018 19:18:50 +0000 (20:18 +0100)]
web site update
additions in a css file