]> matita.cs.unibo.it Git - helm.git/log
helm.git
22 years ago* Scratch window added
Claudio Sacerdoti Coen [Thu, 18 Apr 2002 12:14:36 +0000 (12:14 +0000)]
* Scratch window added
* Check command implemented

22 years agoModified Files:
Irene Schena [Thu, 18 Apr 2002 09:41:19 +0000 (09:41 +0000)]
Modified Files:
1) arith.xsl: ci -> cn for O

22 years ago* Many improvements
Claudio Sacerdoti Coen [Thu, 18 Apr 2002 08:57:10 +0000 (08:57 +0000)]
* Many improvements
* The interface now gives the user the possibility of (re-)opening an existing
  constant.
* Tactic Elim no more exposed in the user interface. Replaced by ElimIntros.
* Selection of subterms in the hypothesis of the goal is now "sound".
* Reduction tactics (Whd, Reduce, Simpl) now work also on the hypothesis.
  New bug/feature: their changes are lost when moving to another goal
  and coming back afterwards.

22 years agoModule Logger added.
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 16:24:03 +0000 (16:24 +0000)]
Module Logger added.

22 years agotype_of_aux' (to get the type of a term in a given environment and context)
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 11:43:12 +0000 (11:43 +0000)]
type_of_aux' (to get the type of a term in a given environment and context)
exported

22 years agopp exported
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 11:40:51 +0000 (11:40 +0000)]
pp exported

22 years agoOoops. Comments in .mly must be delimited by /* and */
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 11:35:25 +0000 (11:35 +0000)]
Ooops. Comments in .mly must be delimited by /* and */

22 years ago* identifiers can now also have digits in them
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 11:34:35 +0000 (11:34 +0000)]
* identifiers can now also have digits in them
* arrow notation for non-dependent Pi-abstraction introduced.
  It seems to be bugged w.r.t. application (a problem of priority?)
* CicTextualParserContext provides an highly not-reentrant implementation
  of parsing in a given environment

22 years ago* Many improvements
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 11:14:07 +0000 (11:14 +0000)]
* Many improvements
* Added the possibility to select parts of the goal of a sequent and retrieve
  the corresponding CIC term.
* New tactics implemented: Cut, Whd, Reduce, Simpl, Change

22 years agoAdded the possibility to select parts of the goal of a sequent and retrieve
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 11:12:53 +0000 (11:12 +0000)]
Added the possibility to select parts of the goal of a sequent and retrieve
the corresponding CIC term.

22 years agoRemoved the patch to avoid a bug of gmetadom.
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 11:11:39 +0000 (11:11 +0000)]
Removed the patch to avoid a bug of gmetadom.

22 years ago...
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 11:09:56 +0000 (11:09 +0000)]
...

22 years agoproofEngineReduction.ml added
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 11:09:39 +0000 (11:09 +0000)]
proofEngineReduction.ml added
It holds functions to perform reduction and simplification of terms.
They are used in the implementation of the reduction/conversion tactics.

22 years ago* Bug fixed: applications of MutCase that are not iota-redexes were reduced
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 09:34:07 +0000 (09:34 +0000)]
* Bug fixed: applications of MutCase that are not iota-redexes were reduced
  just to their head.
* More debugging enabled (to be removed when code becomes stable)

22 years agoInvariant enforced: no Appl of another Appl.
Claudio Sacerdoti Coen [Tue, 16 Apr 2002 09:16:17 +0000 (09:16 +0000)]
Invariant enforced: no Appl of another Appl.

22 years ago1. CicReduction moved into CicReductionNaif
Andrea Asperti [Tue, 16 Apr 2002 09:00:50 +0000 (09:00 +0000)]
1. CicReduction moved into CicReductionNaif
2. CicReductionMachine is the new implementation based on an
   "environment machine".
You must make a sumbolic link from one implementation (.ml) to
cicReduction.ml

22 years agoReplaced with a symbolic link to the actual implementation.
Andrea Asperti [Tue, 16 Apr 2002 08:41:29 +0000 (08:41 +0000)]
Replaced with a symbolic link to the actual implementation.
The symbolic link must be created after check-out.

22 years agotype_of_aux' exported.
Andrea Asperti [Tue, 16 Apr 2002 08:33:53 +0000 (08:33 +0000)]
type_of_aux' exported.

22 years agoMeta implemented.
Andrea Asperti [Tue, 16 Apr 2002 08:33:19 +0000 (08:33 +0000)]
Meta implemented.

22 years agoModified Files:
Irene Schena [Mon, 15 Apr 2002 16:17:20 +0000 (16:17 +0000)]
Modified Files:
1) mmlnotation.xsl xslt_index.txt: MathML default presentation now is
   generated by mmlctop.xsl
Added Files:
1) mmlctop.xsl mmlctop2_0.xsl: link and new Igor stylesheet for MathML default
   presentation

22 years ago* New slides from Saarbrucken
Claudio Sacerdoti Coen [Fri, 12 Apr 2002 17:16:46 +0000 (17:16 +0000)]
* New slides from Saarbrucken
* DTD changed

22 years agoadded debian stuff and a makefile with "dist" target
Stefano Zacchiroli [Fri, 12 Apr 2002 13:39:38 +0000 (13:39 +0000)]
added debian stuff and a makefile with "dist" target

22 years agochanged name to gdome2-xslt
Stefano Zacchiroli [Fri, 12 Apr 2002 13:39:14 +0000 (13:39 +0000)]
changed name to gdome2-xslt

22 years ago- added -fPIC when creating .so
Stefano Zacchiroli [Fri, 12 Apr 2002 13:38:54 +0000 (13:38 +0000)]
- added -fPIC when creating .so
- added PREFIX variable support

22 years agochanged package name to gdome2-xslt
Stefano Zacchiroli [Fri, 12 Apr 2002 13:38:17 +0000 (13:38 +0000)]
changed package name to gdome2-xslt

22 years agocma names parameterized in configure @PACKAGE@ variable
Stefano Zacchiroli [Fri, 12 Apr 2002 13:37:55 +0000 (13:37 +0000)]
cma names parameterized in configure @PACKAGE@ variable

22 years ago-7 debian release, hopefully build also on HPPA
Stefano Zacchiroli [Fri, 12 Apr 2002 12:35:12 +0000 (12:35 +0000)]
-7 debian release, hopefully build also on HPPA

22 years agoadded -fPIC option when compiling ml_gtk_mathview.o
Stefano Zacchiroli [Fri, 12 Apr 2002 12:31:44 +0000 (12:31 +0000)]
added -fPIC option when compiling ml_gtk_mathview.o

22 years agoNew data.
Claudio Sacerdoti Coen [Thu, 11 Apr 2002 08:50:31 +0000 (08:50 +0000)]
New data.

22 years agoFirst MOWGLI paper. Many others will follow.
Claudio Sacerdoti Coen [Wed, 10 Apr 2002 17:44:42 +0000 (17:44 +0000)]
First MOWGLI paper. Many others will follow.

22 years agoThe first MOWGLI paper. Many many others will follow.
Claudio Sacerdoti Coen [Wed, 10 Apr 2002 17:20:05 +0000 (17:20 +0000)]
The first MOWGLI paper. Many many others will follow.

22 years agoDuring the computation of the inner-type of a LAMBDA, the grandfather
Claudio Sacerdoti Coen [Mon, 8 Apr 2002 13:12:00 +0000 (13:12 +0000)]
During the computation of the inner-type of a LAMBDA, the grandfather
was retrieved instead of the father. Fixed.

22 years ago* Many improvements
Claudio Sacerdoti Coen [Mon, 8 Apr 2002 12:57:42 +0000 (12:57 +0000)]
* Many improvements
* Proofs are now rendered in natural language. The inner-types file is
  store in /public/sacerdot/innertypes and directly retrieved from there.
  We must find a better solution.
* Apply tactic now implemented. It is based on the unification stuff of
  Andrea.

22 years agoDeclaration and Definition renamed to Decl and Def because
Claudio Sacerdoti Coen [Mon, 8 Apr 2002 12:54:19 +0000 (12:54 +0000)]
Declaration and Definition renamed to Decl and Def because
Definition was already defined in the DTD.

22 years agoSequent rendering improved: "=======" replaced by a single solid line
Claudio Sacerdoti Coen [Mon, 8 Apr 2002 12:37:18 +0000 (12:37 +0000)]
Sequent rendering improved: "=======" replaced by a single solid line

22 years ago1) Sequent object added.
Claudio Sacerdoti Coen [Mon, 8 Apr 2002 11:05:59 +0000 (11:05 +0000)]
1) Sequent object added.
2) Current Proof and META rendering improved.

22 years ago* Many improvements.
Claudio Sacerdoti Coen [Fri, 5 Apr 2002 09:37:28 +0000 (09:37 +0000)]
* Many improvements.
* Intros and Exact are now implemented.
* Inner sorts are now generated and used.
* Perforation of the proof is now implemented.

22 years agoFirst commit of our future proof-assistant/proof-improver (???)
Claudio Sacerdoti Coen [Tue, 2 Apr 2002 11:53:11 +0000 (11:53 +0000)]
First commit of our future proof-assistant/proof-improver (???)
This commit is based on some un-committed changes to our libraries. So,
it won't compile out-of-the-box.

22 years agoAdded Build-Depends on t1lib-dev
Stefano Zacchiroli [Tue, 2 Apr 2002 08:14:36 +0000 (08:14 +0000)]
Added Build-Depends on t1lib-dev

22 years agoAdded build-depend on libgdome2-cpp-smart-dev.
Stefano Zacchiroli [Mon, 1 Apr 2002 07:46:03 +0000 (07:46 +0000)]
Added build-depend on libgdome2-cpp-smart-dev.

22 years ago- added some .mli and .ml to the debian package
Stefano Zacchiroli [Sun, 31 Mar 2002 22:34:30 +0000 (22:34 +0000)]
- added some .mli and .ml to the debian package
- added depends on libgdome2-ocaml

22 years agopreparing for 0.1.4
Luca Padovani [Sat, 30 Mar 2002 17:39:21 +0000 (17:39 +0000)]
preparing for 0.1.4

22 years agoadded libxml/ in #includes (see libxml2 ChangeLog)
Luca Padovani [Sat, 30 Mar 2002 17:39:01 +0000 (17:39 +0000)]
added libxml/ in #includes (see libxml2 ChangeLog)

22 years agoerror in check for xml2-config
Luca Padovani [Sat, 30 Mar 2002 17:22:13 +0000 (17:22 +0000)]
error in check for xml2-config

22 years agogMathView.mli added
Claudio Sacerdoti Coen [Fri, 29 Mar 2002 09:54:43 +0000 (09:54 +0000)]
gMathView.mli added

22 years agoElectra forms added.
Claudio Sacerdoti Coen [Thu, 28 Mar 2002 17:03:30 +0000 (17:03 +0000)]
Electra forms added.

22 years agoThe contract is now on-line (but for an excel file still missing).
Claudio Sacerdoti Coen [Thu, 28 Mar 2002 14:48:47 +0000 (14:48 +0000)]
The contract is now on-line (but for an excel file still missing).

22 years ago- Increased debian version to 0.3.0-3
Stefano Zacchiroli [Tue, 26 Mar 2002 18:23:16 +0000 (18:23 +0000)]
- Increased debian version to 0.3.0-3
- Added build depends to latest gmetadom and gtkmathview

22 years agoThe compilation of the test is restored.
Claudio Sacerdoti Coen [Tue, 26 Mar 2002 16:06:23 +0000 (16:06 +0000)]
The compilation of the test is restored.
It didn't compile any more due to a different behaviour of gcc on woody.

22 years agoLinks to the version with frames fixed.
Claudio Sacerdoti Coen [Mon, 25 Mar 2002 12:24:05 +0000 (12:24 +0000)]
Links to the version with frames fixed.

22 years agoRendering improved.
Claudio Sacerdoti Coen [Fri, 22 Mar 2002 13:53:21 +0000 (13:53 +0000)]
Rendering improved.

22 years agoRendering improved.
Claudio Sacerdoti Coen [Fri, 22 Mar 2002 13:45:53 +0000 (13:45 +0000)]
Rendering improved.

22 years agoNew MOWGLI member.
Claudio Sacerdoti Coen [Fri, 22 Mar 2002 13:26:09 +0000 (13:26 +0000)]
New MOWGLI member.

22 years agoNew data.
Claudio Sacerdoti Coen [Fri, 22 Mar 2002 13:25:58 +0000 (13:25 +0000)]
New data.

22 years agoLayout improved.
Claudio Sacerdoti Coen [Fri, 22 Mar 2002 13:25:19 +0000 (13:25 +0000)]
Layout improved.

22 years agoframes/no frame switch changed
Luca Padovani [Thu, 21 Mar 2002 20:44:20 +0000 (20:44 +0000)]
frames/no frame switch changed

22 years agoLinks between the versions with and without frames.
Claudio Sacerdoti Coen [Thu, 21 Mar 2002 18:45:49 +0000 (18:45 +0000)]
Links between the versions with and without frames.

22 years agoNew data.
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 17:39:33 +0000 (17:39 +0000)]
New data.

22 years agomowgli-adm mailing list created
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 15:11:43 +0000 (15:11 +0000)]
mowgli-adm mailing list created

22 years agoNew MOWGLI member.
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 15:00:03 +0000 (15:00 +0000)]
New MOWGLI member.

22 years ago* New data
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 14:59:39 +0000 (14:59 +0000)]
* New data
* New members

22 years agoNew data.
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 14:22:56 +0000 (14:22 +0000)]
New data.

22 years agoMOWGLI roles considered in people position
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 12:45:55 +0000 (12:45 +0000)]
MOWGLI roles considered in people position

22 years ago* New MOWGLI members
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 12:18:06 +0000 (12:18 +0000)]
* New MOWGLI members
* New: summary of the MOWGLI kick-off on-line

22 years agoNew data.
Claudio Sacerdoti Coen [Wed, 20 Mar 2002 10:18:47 +0000 (10:18 +0000)]
New data.

22 years agoNew: Minutes of the kick-off
Claudio Sacerdoti Coen [Tue, 19 Mar 2002 18:53:31 +0000 (18:53 +0000)]
New: Minutes of the kick-off

22 years agoPeople in the "by site" list are now sorted alphabetically.
Claudio Sacerdoti Coen [Tue, 19 Mar 2002 17:53:54 +0000 (17:53 +0000)]
People in the "by site" list are now sorted alphabetically.

22 years ago* Some documents were not valid
Claudio Sacerdoti Coen [Tue, 19 Mar 2002 17:35:23 +0000 (17:35 +0000)]
* Some documents were not valid
* Project Leaders added to every package
* New data in project-management

22 years ago* Work Package Leaders added (and rendered)
Claudio Sacerdoti Coen [Mon, 18 Mar 2002 18:49:28 +0000 (18:49 +0000)]
* Work Package Leaders added (and rendered)
* Rendering of Work Packages improved

22 years agoAdded build dep on libgdome2-dev
Stefano Zacchiroli [Fri, 15 Mar 2002 12:25:08 +0000 (12:25 +0000)]
Added build dep on libgdome2-dev

22 years agoDebian changes for version 0.3.0 of lablgtkmathview.
Stefano Zacchiroli [Wed, 13 Mar 2002 23:20:21 +0000 (23:20 +0000)]
Debian changes for version 0.3.0 of lablgtkmathview.
Major changes:
- split shared library package
- debian native package, diff.gz is no longer needed

22 years agoThe contract was the proposal!!!
Claudio Sacerdoti Coen [Wed, 13 Mar 2002 18:43:35 +0000 (18:43 +0000)]
The contract was the proposal!!!

22 years agoData refined.
Claudio Sacerdoti Coen [Wed, 13 Mar 2002 10:24:18 +0000 (10:24 +0000)]
Data refined.

22 years agoInitial version.
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 18:03:32 +0000 (18:03 +0000)]
Initial version.

22 years ago* Linking was still static for native compilation.
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 17:41:44 +0000 (17:41 +0000)]
* Linking was still static for native compilation.
* Automatic compilation of the test in native mode can no more be performed
  because the dynamic library is always searched in the position where
  it will be installed ;-(

22 years agoData refined.
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 15:45:15 +0000 (15:45 +0000)]
Data refined.

22 years agoMore data.
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 11:46:45 +0000 (11:46 +0000)]
More data.

22 years agoNew data.
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 10:35:03 +0000 (10:35 +0000)]
New data.

22 years agoNew Data (operative commencement date).
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 10:28:39 +0000 (10:28 +0000)]
New Data (operative commencement date).

22 years agoNew data.
Claudio Sacerdoti Coen [Tue, 12 Mar 2002 10:18:55 +0000 (10:18 +0000)]
New data.

22 years agoGoguadze added.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 18:02:34 +0000 (18:02 +0000)]
Goguadze added.

22 years agoNew sources by Paul Libbrecht. From these sources it is possible to
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 16:05:17 +0000 (16:05 +0000)]
New sources by Paul Libbrecht. From these sources it is possible to
produce both a nice PDF file and the PS document.

22 years agoLink to Paul's new MOWGLI page added.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 15:51:47 +0000 (15:51 +0000)]
Link to Paul's new MOWGLI page added.

22 years agoModified Files:
Irene Schena [Mon, 11 Mar 2002 15:51:08 +0000 (15:51 +0000)]
Modified Files:
1) dfki.xml: added member

22 years agoNot well-formed XML.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 15:44:36 +0000 (15:44 +0000)]
Not well-formed XML.

22 years agoPaul Libbrecht added.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 15:36:15 +0000 (15:36 +0000)]
Paul Libbrecht added.

22 years agoModified Files:
Irene Schena [Mon, 11 Mar 2002 14:39:53 +0000 (14:39 +0000)]
Modified Files:
1) html/Makefile html/proposal/.cvsignore xml/home.xml
   xml/menu.xml xml/project.xml xml/proposal/EC-contribution.xml
   xml/proposal/contribution.xml
   xml/proposal/econ-scient-tech-prospects.xml
   xml/proposal/innovation.xml
   xml/proposal/project-components.xml
   xml/proposal/project-management.xml
   xml/proposal/project-objectives.xml
   xml/proposal/project-planning.xml
   xml/proposal/project-summary.xml xsl/project.xsl: now the proposal index is
   in project.xml that is linked in the Project Menu
Removed Files:
1) xml/proposal/proposal-index.xml: now is in project.xml

22 years agoModified Files:
Irene Schena [Mon, 11 Mar 2002 13:21:25 +0000 (13:21 +0000)]
Modified Files:
1) xml/sites/aei.xml xml/sites/dfki.xml xml/sites/nijmegen.xml
   xml/sites/trusted-logic.xml xsl/site.xsl: added site members info

22 years agoModified Files:
Irene Schena [Mon, 11 Mar 2002 12:01:51 +0000 (12:01 +0000)]
Modified Files:
1) xml/home.xml xml/proposal/EC-contribution.xml
   xml/proposal/contribution.xml
   xml/proposal/econ-scient-tech-prospects.xml
   xml/proposal/innovation.xml
   xml/proposal/project-components.xml
   xml/proposal/project-management.xml
   xml/proposal/project-objectives.xml
   xml/proposal/project-planning.xml
   xml/proposal/project-summary.xml xml/sites/dfki.xml: bugs fixed

22 years agoNew data.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 11:27:38 +0000 (11:27 +0000)]
New data.

22 years agoMarkus Moschner (DFKI) added.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 11:27:03 +0000 (11:27 +0000)]
Markus Moschner (DFKI) added.

22 years agoMarkus Moschner (DFKI) added.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 11:21:53 +0000 (11:21 +0000)]
Markus Moschner (DFKI) added.

22 years agoA much better PDF file contributed by Paul Libbrecht.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 11:00:47 +0000 (11:00 +0000)]
A much better PDF file contributed by Paul Libbrecht.

22 years agoLink to ActiveMath added.
Claudio Sacerdoti Coen [Mon, 11 Mar 2002 11:00:16 +0000 (11:00 +0000)]
Link to ActiveMath added.

22 years agoModified Files:
Irene Schena [Fri, 8 Mar 2002 16:40:51 +0000 (16:40 +0000)]
Modified Files:
1) sites/dfki.xml sites/nijmegen.xml: errors fixed

22 years agoModified Files:
Irene Schena [Fri, 8 Mar 2002 16:15:40 +0000 (16:15 +0000)]
Modified Files:
1) asperti.xml guidi.xml padovani.xml sacerdoti.xml schena.xml: info updated

22 years agoloadDocumentFrom* and saveDocument interface changed
Claudio Sacerdoti Coen [Fri, 8 Mar 2002 12:19:13 +0000 (12:19 +0000)]
loadDocumentFrom* and saveDocument interface changed

22 years agoModified Files:
Irene Schena [Fri, 8 Mar 2002 12:03:40 +0000 (12:03 +0000)]
Modified Files:
1) pert_new.png: added resolution

22 years ago-rpath used to record the path to use to search for dynamic libraries
Claudio Sacerdoti Coen [Wed, 6 Mar 2002 18:14:53 +0000 (18:14 +0000)]
-rpath used to record the path to use to search for dynamic libraries
which are not in LD_LIBRARY_PATH. (In our case, all the dynamic libraries
of the bindings this one depends on.)

22 years agoThe .so file was not moved into the temporary installation directory.
Claudio Sacerdoti Coen [Wed, 6 Mar 2002 17:20:23 +0000 (17:20 +0000)]
The .so file was not moved into the temporary installation directory.