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

porting to recent ocaml

...

lablgtk3.sourceview3 => lablgtk3-sourceview3

patches for compilation with ocaml 4.0.5

+ lambdadelta website update

finite_lambda restored

reverse_complexity lib restored

the toolkit.ma file contains errors. I have
commented out a few places

make depend.opt

make dist repaired

- svn export => git archive

version upgrade

added missing libs detection

Most warnings turned into errors and avoided

0.99.3 -> 0.99.4

report_error dialog ported to gtk3

Quit without saving dialog fixed

Ported to gtk3

useful comment

automatically inserted aliases

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.

use #run for dialog

Let the widget expand in the old way

Old glade2 file removed

Broken libs moved to broken_lib

Some can probably be restored with some love.

lablgladecc => lablgladecc3

It now compiles with lablgtk3 opam package

disambiguationErrors now uses #run

correct Gtk behavior

code for DisambiguationErrors simplified

Still not working (since matita 0.99x?)

several dialog boxes no longer used removed

they were dead code in current Matita
I only left the AutoWin and the ones used

last deprecated widget updated

findReplace ported from GtkTable to GtkGrid

More H/V deprecated widgets replaced

GtkHSeparator deprecated

GtkSeparator used instead

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.

comment

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

Fix dialog win

It used to be destroyed when closed the first time

Use lablgladecc -embed again

On-going porting to lablgtk3

update in basic_2

+ main result on acle proved

update in static_2

+ preorder on applicability domains
+ minor bug fixes

new web site page

change log for λδ begins

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

milestone in basic_2

We parametrize applicability condition with a generic subset of numbers.

update in static_2 and basic_2

+ a weaker version of tueq reintroduced
+ some renaming
+ one conjecture to prove

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 ...

still more additions and corrections for the article

+ one theorem was missing
+ some renaming

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

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

additions and corrections for the article on λδ-2B

+ candidates: condition S4 removed
+ arity assignment: decidability proved
+ minor additions

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

some restyling ...

+ fixing some notations
+ fixing some spaces

milestone in basic_2

+ Parametrized applicability condition allows λδ-2B to generalize both λδ-1A and λδ-1B.
+ ground_2: minor additions

update in basic_2

one file was missing in last commit :(

update in basic_2

+ totality for fixed cpce
+ Makefile: bug fixed

decentralizing core notation continues ...

+ apart, napart decentralized

update in basic_2

+ decidability of type inference
+ decidability of type checking

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

update in basic_2

+ decidability of cpes
+ some renaming

update in ground_2 static_2 basic_2

structures for decidability of the validity predicate

+ cpes, cnr, cpre resumed
+ minor corrections

milestone in basic_2

preservation of validity for rt-computation does not need the sort degree parameter (i.e. no induction on the degree).

update in ground_2 static_2 basic_2

+ whd normal forms for terms with arity
+ positive abbreviations are not whd normal forms
+ minor additions

first steps towards decidability of the validity predicate

+ tentative definition of cwhx

minor corrections and updates

intensional and extensional equivalence on lists coincide

patches for compilation with ocaml 4.0.5

+ lambdadelta website update

the decentralization of core notation continues ...

subseteq notation decentralized

finite_lambda restored

reverse_complexity lib restored

the toolkit.ma file contains errors. I have
commented out a few places

make depend.opt

make dist repaired

- svn export => git archive

version upgrade

added missing libs detection

Most warnings turned into errors and avoided

0.99.3 -> 0.99.4

report_error dialog ported to gtk3

Quit without saving dialog fixed

Ported to gtk3

useful comment

automatically inserted aliases

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.

use #run for dialog

Let the widget expand in the old way

Old glade2 file removed

Broken libs moved to broken_lib

Some can probably be restored with some love.

lablgladecc => lablgladecc3

It now compiles with lablgtk3 opam package

disambiguationErrors now uses #run

correct Gtk behavior

code for DisambiguationErrors simplified

Still not working (since matita 0.99x?)

several dialog boxes no longer used removed

they were dead code in current Matita
I only left the AutoWin and the ones used

last deprecated widget updated

findReplace ported from GtkTable to GtkGrid

More H/V deprecated widgets replaced

GtkHSeparator deprecated

GtkSeparator used instead

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.

comment

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

Fix dialog win

It used to be destroyed when closed the first time

Use lablgladecc -embed again

xoa utility updated

+ two missing cases implemented
+ dependences fixed in Makefile

On-going porting to lablgtk3

list of failing files updated

+ one file added

web site update

one css stylesheet improved

web site update

+ one css file improved

web site update

additions in a css file

supplementary files for web site

+ css file name corrected