]> matita.cs.unibo.it Git - helm.git/log
helm.git
13 years agothe thinning lemma follows immediately from the substitution lemma ...
Ferruccio Guidi [Tue, 22 Mar 2011 20:34:05 +0000 (20:34 +0000)]
the thinning lemma follows immediately from the substitution lemma ...

13 years ago- lambda_notation.ma: more notation and bug fixes
Ferruccio Guidi [Tue, 22 Mar 2011 18:53:26 +0000 (18:53 +0000)]
- lambda_notation.ma: more notation and bug fixes
- terms.ma: contains the data structure of terms and related functions (not involving substitution).
- ext_lambda.ma: cut off of previous ext.ma, containing the lambda-related objects
- subst.ma, types.ma: we removed notation from here
- types.ma: we added special cases of the weakening and thinning lemmas as axioms

13 years agoBug fixed and code refactoring: now both matitac and matita include files
Claudio Sacerdoti Coen [Tue, 22 Mar 2011 17:22:53 +0000 (17:22 +0000)]
Bug fixed and code refactoring: now both matitac and matita include files
correctly by re-generating ~include_paths in the same way and every time a
file is opened (either by matitaScript or by assert_ng itself).

13 years agoUse matita/lib as the new standard library in place of matita/nlibrary.
Claudio Sacerdoti Coen [Tue, 22 Mar 2011 16:41:24 +0000 (16:41 +0000)]
Use matita/lib as the new standard library in place of matita/nlibrary.

13 years agoDebugging code removed.
Claudio Sacerdoti Coen [Tue, 22 Mar 2011 16:39:35 +0000 (16:39 +0000)]
Debugging code removed.

13 years agosn_prod
Andrea Asperti [Mon, 21 Mar 2011 08:18:22 +0000 (08:18 +0000)]
sn_prod

13 years agosn_lambda
Andrea Asperti [Mon, 21 Mar 2011 07:41:43 +0000 (07:41 +0000)]
sn_lambda

13 years agoextensions
Andrea Asperti [Mon, 21 Mar 2011 07:40:56 +0000 (07:40 +0000)]
extensions

13 years agoBug "fixed" (i.e avoided).
Claudio Sacerdoti Coen [Sat, 19 Mar 2011 00:00:31 +0000 (00:00 +0000)]
Bug "fixed" (i.e avoided).

Bug description:
 - matitac (more precisely, MatitaEngine.assert_ng, hence the "include"
   command) parses files differently from Matita. In particular, it works on
   a camlp5 "Grammar.parsable" lexer, which is a lexer that remembers
   look-ahead tokens.
 - an "include" file can change the list of keywords for the lexer
   (e.g. when defining the "if-then-else" notation). Hence, after an include,
   the lexer to be used must change and thus the corresponding
   "Grammar.parsable" should change too. This was not the case since the
   "Grammar.parsable" was not regenerated to avoid loosing the look-ahead
   tokens

Bug avoidance:
 - we assume that the "include" command is properly terminated. Hence no
   look-ahead is performed. After each "include" command we regenerate
   the lexer to avoid the bug.

Note:
 - why don't we need to do this just after a "notation" command?
   Apparently, this is not required. However, I do not understand why.
   Is this to be better understood in the future?

13 years agoPorted to
Claudio Sacerdoti Coen [Fri, 18 Mar 2011 16:03:55 +0000 (16:03 +0000)]
Ported to

- camlp5 version 6.02.2 + patches
- ocaml version 3.11.2-4

If you are still using the old version of OCaml + Camlp5, do not update
these two files.

13 years ago- more notation and service lemmas
Ferruccio Guidi [Tue, 15 Mar 2011 19:18:39 +0000 (19:18 +0000)]
- more notation and service lemmas
- arity.ma: arities and arity types
- arity_eval.ma: arities and arity types assigned to terms

13 years ago- some ignores
Ferruccio Guidi [Tue, 15 Mar 2011 12:03:55 +0000 (12:03 +0000)]
- some ignores
- new service lemmas

13 years agodependences fix
Ferruccio Guidi [Mon, 14 Mar 2011 21:19:49 +0000 (21:19 +0000)]
dependences fix

13 years agoadded star.ma (star closure of a relation)
Andrea Asperti [Fri, 11 Mar 2011 07:17:06 +0000 (07:17 +0000)]
added star.ma (star closure of a relation)

13 years agoImprovements.
Andrea Asperti [Fri, 11 Mar 2011 07:15:20 +0000 (07:15 +0000)]
Improvements.

13 years agodiamond property
Andrea Asperti [Thu, 10 Mar 2011 07:41:22 +0000 (07:41 +0000)]
diamond property

13 years agomore notation and all-purpose lemmas
Ferruccio Guidi [Wed, 9 Mar 2011 21:06:55 +0000 (21:06 +0000)]
more notation and all-purpose lemmas

13 years agothe interpretation for Sigma was missing
Ferruccio Guidi [Wed, 9 Mar 2011 11:59:38 +0000 (11:59 +0000)]
the interpretation for Sigma was missing

13 years agoFirst commit with new (incomplete) disambiguation engine.
Wilmer Ricciotti [Tue, 8 Mar 2011 13:26:37 +0000 (13:26 +0000)]
First commit with new (incomplete) disambiguation engine.

13 years agosottotermini e confluenza (manca pr_substs).
Andrea Asperti [Mon, 7 Mar 2011 07:29:04 +0000 (07:29 +0000)]
sottotermini e confluenza (manca pr_substs).

13 years agowe started the implementation of higher order saturated sets
Ferruccio Guidi [Wed, 2 Mar 2011 21:02:38 +0000 (21:02 +0000)]
we started the implementation of higher order saturated sets

13 years ago- rc_sat.ma: we changed the notation for extensional equality. we now
Ferruccio Guidi [Sun, 27 Feb 2011 18:27:15 +0000 (18:27 +0000)]
- rc_sat.ma: we changed the notation for extensional equality. we now
use \cong like in geometry
- rc_eval.ma (second part of former rc_ma): we completed the evaluation
by adding a stack, and we proved weakening and thinning for it

13 years ago- notation is now in a separate file
Ferruccio Guidi [Sun, 27 Feb 2011 15:31:29 +0000 (15:31 +0000)]
- notation is now in a separate file
- sn.ma: we updated the axiomatization of SN while correcting the saturation
conditions
- rc_sat.ma: we proved that depRC is a candidate

13 years ago- new file ext.ma with the objects needed for the normalization so
Ferruccio Guidi [Sat, 26 Feb 2011 20:28:06 +0000 (20:28 +0000)]
- new file ext.ma with the objects needed for the normalization so
far, that should be removed or should go into other files
- sn.ma: we parametrized the saturation conditions
- rc_sat.ma (first part of former rc.ma): we introduced extensional
equality on candidates

13 years agowe started to set up the strong normalization proof.
Ferruccio Guidi [Mon, 21 Feb 2011 19:05:11 +0000 (19:05 +0000)]
we started to set up the strong normalization proof.
we plan to use saturated subsets of strongly normalizing terms
(see for instance D. Cescutti 2001, but a better citation is required)
rather than reducibility candidates.
The benefit is that reduction is not needed to define such subsets.
Also, this approach was never tried on a system with dependent types.

13 years agofork for Matita version B
Wilmer Ricciotti [Mon, 21 Feb 2011 13:25:29 +0000 (13:25 +0000)]
fork for Matita version B

13 years agowe added some comments
Ferruccio Guidi [Thu, 10 Feb 2011 15:41:24 +0000 (15:41 +0000)]
we added some comments

13 years agoAdded typing rule for dummies
Andrea Asperti [Thu, 10 Feb 2011 12:19:56 +0000 (12:19 +0000)]
Added typing rule for dummies

13 years agoAdded lambda
Andrea Asperti [Thu, 10 Feb 2011 11:55:27 +0000 (11:55 +0000)]
Added lambda

13 years agoenabling destruct defs
Wilmer Ricciotti [Wed, 9 Feb 2011 14:33:40 +0000 (14:33 +0000)]
enabling destruct defs

13 years agoHyperlinks are back.
Claudio Sacerdoti Coen [Thu, 27 Jan 2011 15:52:16 +0000 (15:52 +0000)]
Hyperlinks are back.

13 years agoHyperlinks are now computed correctly. I least I hope...
Claudio Sacerdoti Coen [Thu, 27 Jan 2011 14:58:12 +0000 (14:58 +0000)]
Hyperlinks are now computed correctly. I least I hope...

13 years agoRemoved inclusion of logic/equality.ma in datatypes/list.ma (not needed and
Wilmer Ricciotti [Fri, 21 Jan 2011 13:30:33 +0000 (13:30 +0000)]
Removed inclusion of logic/equality.ma in datatypes/list.ma (not needed and
source of conflicts in other scripts).

13 years agoBugfix for elimination principles.
Wilmer Ricciotti [Thu, 20 Jan 2011 13:54:38 +0000 (13:54 +0000)]
Bugfix for elimination principles.

13 years agoBug fix for generation of elimination principles.
Wilmer Ricciotti [Thu, 20 Jan 2011 13:41:41 +0000 (13:41 +0000)]
Bug fix for generation of elimination principles.

13 years agoAdded some typing info to elimination principles, allowing the refiner
Wilmer Ricciotti [Wed, 19 Jan 2011 11:29:14 +0000 (11:29 +0000)]
Added some typing info to elimination principles, allowing the refiner
to succeed in more cases, also speeding up the generation process (no
more slow record definitions).

13 years agoAdded some typing info to elimination principles, allowing the refiner
Wilmer Ricciotti [Wed, 19 Jan 2011 11:06:23 +0000 (11:06 +0000)]
Added some typing info to elimination principles, allowing the refiner
to succeed in more cases, also speeding up the generation process (no
more slow record definitions).

13 years agoThe sequent window now always scroll to the bottom when its content changes.
Claudio Sacerdoti Coen [Fri, 14 Jan 2011 14:15:00 +0000 (14:15 +0000)]
The sequent window now always scroll to the bottom when its content changes.

13 years agoBug fixed: the script windows did not scroll correctly because I used the
Claudio Sacerdoti Coen [Fri, 14 Jan 2011 12:10:42 +0000 (12:10 +0000)]
Bug fixed: the script windows did not scroll correctly because I used the
wrong method.

13 years agoctrl+pgUp/Down to navigate tabs
Enrico Tassi [Tue, 11 Jan 2011 22:26:45 +0000 (22:26 +0000)]
ctrl+pgUp/Down to navigate tabs

13 years agoctrl+pgUp/Down to navigate tabs
Enrico Tassi [Tue, 11 Jan 2011 22:25:40 +0000 (22:25 +0000)]
ctrl+pgUp/Down to navigate tabs

13 years ago...
Claudio Sacerdoti Coen [Tue, 11 Jan 2011 22:03:04 +0000 (22:03 +0000)]
...

13 years agoBug fixed: the newScript method must be called only after registering the
Claudio Sacerdoti Coen [Tue, 11 Jan 2011 22:02:11 +0000 (22:02 +0000)]
Bug fixed: the newScript method must be called only after registering the
gui. I have moved the invocation of self#newScript from the initializer to the
instance() function to solve the issue (an ugly gtk error when Matita starts).

13 years agoBug fixed: the accelerators for Close and Quit were both Ctrl+q (???)
Claudio Sacerdoti Coen [Tue, 11 Jan 2011 21:49:52 +0000 (21:49 +0000)]
Bug fixed: the accelerators for Close and Quit were both Ctrl+q (???)

13 years agoLast commit reverted (it was an error).
Claudio Sacerdoti Coen [Tue, 11 Jan 2011 21:35:34 +0000 (21:35 +0000)]
Last commit reverted (it was an error).

13 years agoPart of last HUGE COMMIT about NCic.status
Claudio Sacerdoti Coen [Tue, 11 Jan 2011 21:29:25 +0000 (21:29 +0000)]
Part of last HUGE COMMIT about NCic.status

13 years agoStupid bug fixed (introduced a couple of commits ago): the close button for
Claudio Sacerdoti Coen [Tue, 11 Jan 2011 21:18:17 +0000 (21:18 +0000)]
Stupid bug fixed (introduced a couple of commits ago): the close button for
tabs always closed the first tab instead of the right one.

13 years agoHUGE COMMIT:
Claudio Sacerdoti Coen [Tue, 11 Jan 2011 21:06:37 +0000 (21:06 +0000)]
HUGE COMMIT:

1) sequent2pres merged into content2pres
2) more functions to render sequents/context/substs to content and then to
   presentation
3) new virtual class NCic.status with methods implementing pretty-printing
   functions (same interface that used to be given in NCicPp); objects of this
   class are now used REALLY ALL OVER the matita code (well, almost...)
4) NCicPp implements a concrete version of NCic.status
   (low level pretty-printer)
5) ApplyTransformation implements a concrete version of NCic.status
   (high level pretty-printer that uses notation). It also exports the boolean
   reference to deactivate the high level pretty printer in favour of the
   low level one
6) some code simplifications here and there (in particular for tactics)
7) return type of BoxPp changed to yield informations about hyperlinks;
   the information is not used yet by the interface and it is not computed
   yet (not that easy to do...)
8) other minor stuff here and there

13 years agocoercion lookup now returns coercions ranked using the number of symbols matched...
Enrico Tassi [Tue, 11 Jan 2011 15:12:32 +0000 (15:12 +0000)]
coercion lookup now returns coercions ranked using the number of symbols matched, the more precise match first

13 years agocode simplification
Claudio Sacerdoti Coen [Mon, 10 Jan 2011 16:13:13 +0000 (16:13 +0000)]
code simplification

13 years ago...
Enrico Tassi [Fri, 7 Jan 2011 22:01:00 +0000 (22:01 +0000)]
...

13 years agoadded retrieval function with weight
Enrico Tassi [Fri, 7 Jan 2011 21:52:48 +0000 (21:52 +0000)]
added retrieval function with weight

13 years agonon uniform coercion names in sync with the TYPES talk, stil commented out...
Enrico Tassi [Fri, 7 Jan 2011 14:00:29 +0000 (14:00 +0000)]
non uniform coercion names in sync with the TYPES talk, stil commented out...

13 years ago...
Enrico Tassi [Fri, 7 Jan 2011 13:55:48 +0000 (13:55 +0000)]
...

13 years ago...
Claudio Sacerdoti Coen [Mon, 3 Jan 2011 14:17:06 +0000 (14:17 +0000)]
...

13 years ago...
Claudio Sacerdoti Coen [Mon, 3 Jan 2011 14:02:29 +0000 (14:02 +0000)]
...

13 years agoBrainstorming
Claudio Sacerdoti Coen [Mon, 3 Jan 2011 14:00:56 +0000 (14:00 +0000)]
Brainstorming

13 years agoops, we forgot to update the version indicator :)
Ferruccio Guidi [Sun, 2 Jan 2011 15:55:14 +0000 (15:55 +0000)]
ops, we forgot to update the version indicator :)

13 years ago- ld-html-root: ported to permanent lambda-delta url
Ferruccio Guidi [Sun, 2 Jan 2011 15:47:01 +0000 (15:47 +0000)]
- ld-html-root: ported to permanent lambda-delta url
- ld.dtd: we can specify a language encoding for the metalinguistic
annotation, moreover we export the metalinguistic classification
- the other files are modified in order to support this feature

13 years agoBugs and other stuff to do to complete the Matita 1/2 => Matita 1.0 transition.
Claudio Sacerdoti Coen [Tue, 28 Dec 2010 22:10:10 +0000 (22:10 +0000)]
Bugs and other stuff to do to complete the Matita 1/2 => Matita 1.0 transition.

13 years agoInterface reduction; code clean up.
Claudio Sacerdoti Coen [Tue, 28 Dec 2010 21:51:28 +0000 (21:51 +0000)]
Interface reduction; code clean up.

13 years agocode simplification
Claudio Sacerdoti Coen [Tue, 28 Dec 2010 21:27:29 +0000 (21:27 +0000)]
code simplification

13 years agoCode clean up.
Claudio Sacerdoti Coen [Tue, 28 Dec 2010 20:38:30 +0000 (20:38 +0000)]
Code clean up.

13 years agoDead code removed.
Claudio Sacerdoti Coen [Tue, 28 Dec 2010 20:10:50 +0000 (20:10 +0000)]
Dead code removed.

13 years agoMore code clean-up.
Claudio Sacerdoti Coen [Tue, 28 Dec 2010 17:42:07 +0000 (17:42 +0000)]
More code clean-up.

13 years agoUseless code removed; interfaces simplified; etc.
Claudio Sacerdoti Coen [Tue, 28 Dec 2010 17:21:43 +0000 (17:21 +0000)]
Useless code removed; interfaces simplified; etc.

13 years ago1. reset of statuses simplified
Claudio Sacerdoti Coen [Mon, 27 Dec 2010 21:51:13 +0000 (21:51 +0000)]
1. reset of statuses simplified
2. NCicEnvironment.invalidate_all (that used to hide a bug in invalidation)
   removed. The semantics of the MTI is now more shacky, but this needs to be
   fixed in other ways.
3. {lexicon_,grafite_,...}status renamed into status

13 years agoSome comments (new problems found).
Claudio Sacerdoti Coen [Mon, 27 Dec 2010 20:58:08 +0000 (20:58 +0000)]
Some comments (new problems found).

13 years agoReally A LOT of code to add close buttons to the tab labels :-(
Claudio Sacerdoti Coen [Thu, 23 Dec 2010 22:15:35 +0000 (22:15 +0000)]
Really A LOT of code to add close buttons to the tab labels :-(

13 years agoBug fixed (introduced in previous commit): opening multiple files requires first
Claudio Sacerdoti Coen [Thu, 23 Dec 2010 22:14:44 +0000 (22:14 +0000)]
Bug fixed (introduced in previous commit): opening multiple files requires first
the creation of the newScript to be replaced.

13 years agoImplemented standard semantics of Load in MTI: loading a file when the current
Claudio Sacerdoti Coen [Thu, 23 Dec 2010 15:13:41 +0000 (15:13 +0000)]
Implemented standard semantics of Load in MTI: loading a file when the current
one is unnamed and not modified does not open a new tab.

13 years ago1. MatitaGuiTypes.gui interface streamlined
Claudio Sacerdoti Coen [Thu, 23 Dec 2010 15:06:10 +0000 (15:06 +0000)]
1. MatitaGuiTypes.gui interface streamlined
2. added new menu item to close a script
3. restored graying of "Save" menu item when the script is unnamed

13 years agoAvoid duplicates in the list.
Andrea Asperti [Thu, 23 Dec 2010 12:13:32 +0000 (12:13 +0000)]
Avoid duplicates in the list.

13 years ago1. bug fixed: in the last commit on NCicLibrary we forgot that
Andrea Asperti [Thu, 23 Dec 2010 12:11:57 +0000 (12:11 +0000)]
1. bug fixed: in the last commit on NCicLibrary we forgot that
   get_already_included must be transitively closed; fixed and changed
   the function name
2. added a cache to assert_ng (called ~asserted) to avoid re-asserting
   the same file twice during a single include command

13 years ago1. bug in addition of universe constraints fixed: the recursive
Andrea Asperti [Thu, 23 Dec 2010 10:32:44 +0000 (10:32 +0000)]
1. bug in addition of universe constraints fixed: the recursive
   inclusion does not add constraints to the NCicLibrary.storage
2. since we no longer perform recursive cleaning,
   NCicEnvironment.invalidate_item is no longer recursive. This fixed
   definitely the bugs in undo/redo linked to "include"s

13 years agoprogress
Andrea Asperti [Thu, 23 Dec 2010 09:24:39 +0000 (09:24 +0000)]
progress

13 years agomore theory for lists
Wilmer Ricciotti [Wed, 22 Dec 2010 17:37:18 +0000 (17:37 +0000)]
more theory for lists

13 years ago...
Wilmer Ricciotti [Wed, 22 Dec 2010 16:37:30 +0000 (16:37 +0000)]
...

13 years agoUseless code removed.
Claudio Sacerdoti Coen [Tue, 21 Dec 2010 17:01:01 +0000 (17:01 +0000)]
Useless code removed.

13 years agoDead and useless code removed.
Claudio Sacerdoti Coen [Tue, 21 Dec 2010 16:37:25 +0000 (16:37 +0000)]
Dead and useless code removed.

13 years agoDead code removed.
Claudio Sacerdoti Coen [Tue, 21 Dec 2010 15:54:00 +0000 (15:54 +0000)]
Dead code removed.

13 years agoWhen switching to a new script, the other parts of the interface are
Claudio Sacerdoti Coen [Tue, 21 Dec 2010 15:14:47 +0000 (15:14 +0000)]
When switching to a new script, the other parts of the interface are
now notified.

13 years ago...
Claudio Sacerdoti Coen [Tue, 21 Dec 2010 14:42:23 +0000 (14:42 +0000)]
...

13 years agoVERY EXPERIMENTAL:
Claudio Sacerdoti Coen [Tue, 21 Dec 2010 14:42:08 +0000 (14:42 +0000)]
VERY EXPERIMENTAL:

first version of Matita as a Tabbed Document Interface.

The semantics of working on two tabs at the same time is not defined
(yet? ...)

13 years ago...
Claudio Sacerdoti Coen [Tue, 21 Dec 2010 01:11:15 +0000 (01:11 +0000)]
...

13 years agoCode clean-up
Claudio Sacerdoti Coen [Mon, 20 Dec 2010 17:42:37 +0000 (17:42 +0000)]
Code clean-up

13 years agoLarge commit: refactoring of the code of the interface.
Claudio Sacerdoti Coen [Mon, 20 Dec 2010 17:24:55 +0000 (17:24 +0000)]
Large commit: refactoring of the code of the interface.

1. management of font sizes centralized in MatitaMisc according to the
   MVC paradigm
2. functionalities related to the script window moved from MatitaGui to
   MatitaScript

13 years agoFirst steps towards a multi-document interface.
Claudio Sacerdoti Coen [Mon, 20 Dec 2010 13:14:15 +0000 (13:14 +0000)]
First steps towards a multi-document interface.

13 years agoClass mathViewer got rid of. The circular dependency between
Claudio Sacerdoti Coen [Sun, 19 Dec 2010 20:28:10 +0000 (20:28 +0000)]
Class mathViewer got rid of. The circular dependency between
the scripts needs to be sorted out by putting matitaScript much
later in the chain. This commit temporary introduces bad type
expressions here and there.

13 years ago1. Method screenshot moved to CicMathView where it belongs to.
Claudio Sacerdoti Coen [Sun, 19 Dec 2010 19:52:37 +0000 (19:52 +0000)]
1. Method screenshot moved to CicMathView where it belongs to.
2. the mutual dependency between MatitaScript and CicMathView/MatitaMathView
   needs to be solved differently (it used to be solved using guistuff, which
   I do not consider any longer a good solution). To be done.

With this commit, anything related to MathML vs Textual is now in
cicMathView.ml.

13 years agoUseless methods removed.
Claudio Sacerdoti Coen [Sat, 18 Dec 2010 23:37:08 +0000 (23:37 +0000)]
Useless methods removed.

13 years ago1) matitaMathView.ml splitted into cicMathView.ml + matitaMathView.ml
Claudio Sacerdoti Coen [Sat, 18 Dec 2010 23:27:37 +0000 (23:27 +0000)]
1) matitaMathView.ml splitted into cicMathView.ml + matitaMathView.ml
2) interface of matitaMathView.ml and cicMathView.ml greatly simplifed
   so to avoid any reference to the textual/MathML datatypes.
3) up to the problem of taking screenshots, the file matitaMathView.ml
   is now oblivious of the difference between text and MathML. It will
   be soon possible to switch between text and MathML simply by changing
   the implementation of cicMathView.

13 years agoBetter typing.
Claudio Sacerdoti Coen [Fri, 17 Dec 2010 23:35:27 +0000 (23:35 +0000)]
Better typing.

13 years agoNow useless type declaration removed.
Claudio Sacerdoti Coen [Fri, 17 Dec 2010 22:50:44 +0000 (22:50 +0000)]
Now useless type declaration removed.

13 years agoThis commit simplifies the interfaces of the various Widget-related .mli
Claudio Sacerdoti Coen [Fri, 17 Dec 2010 22:45:29 +0000 (22:45 +0000)]
This commit simplifies the interfaces of the various Widget-related .mli
files, so that the same inferfaces can be used both for the MathMl widget and
the textual widget.

Practically, it is now sufficient to switch between two implementations of
matitaMathView to change between MathML/textual.

13 years agoLarge commit:
Claudio Sacerdoti Coen [Thu, 16 Dec 2010 17:10:54 +0000 (17:10 +0000)]
Large commit:

1) some dead code removed
2) code of MatitaClean commented out (but still there for disambiguation and
   the like?)
3) dependencies and uris moved into dumpable_status (from other statuses
   and/or imperative code) and made functional
4) all the bugs related to recursive compilation seem to have been fixed by 3)

13 years agoNew version of the library. Several files still do not compile.
Andrea Asperti [Thu, 16 Dec 2010 11:54:35 +0000 (11:54 +0000)]
New version of the library. Several files still do not compile.

13 years agoSome bugs fixed (and some still open) in recursive compilation of files:
Andrea Asperti [Thu, 16 Dec 2010 11:51:30 +0000 (11:51 +0000)]
Some bugs fixed (and some still open) in recursive compilation of files:
 a) matitac now takes again either a list of files to be compiled or
    nothing (to compile all files in the cwd)
 b) ...

13 years agoBug fixed: a file A that includes a file B needs to be recompiled also
Andrea Asperti [Thu, 16 Dec 2010 10:13:57 +0000 (10:13 +0000)]
Bug fixed: a file A that includes a file B needs to be recompiled also
when B has been compiled after A.

13 years agoDead code removed.
Andrea Asperti [Thu, 16 Dec 2010 10:13:08 +0000 (10:13 +0000)]
Dead code removed.