]> matita.cs.unibo.it Git - helm.git/log
helm.git
22 years agoComputed inner-types are now also put in whd normal form.
Claudio Sacerdoti Coen [Mon, 29 Apr 2002 10:22:09 +0000 (10:22 +0000)]
Computed inner-types are now also put in whd normal form.
This is at the same type too strong (e.g. it performs delta-reductions)
and too weak (it is not full-reduction).
We can consider this just a patch waiting for Coscoy's double-inference
algorithm implementation.

22 years agoBug fixed: the unwinding was not recursively performed. (a "t" should have been
Claudio Sacerdoti Coen [Mon, 29 Apr 2002 10:07:47 +0000 (10:07 +0000)]
Bug fixed: the unwinding was not recursively performed. (a "t" should have been
a "t'")

22 years agoMETA parsing was completely broken. Fixed.
Claudio Sacerdoti Coen [Mon, 29 Apr 2002 10:06:06 +0000 (10:06 +0000)]
META parsing was completely broken. Fixed.

22 years agogdome_xslt ==> gdome2-xslt
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 13:54:49 +0000 (13:54 +0000)]
gdome_xslt ==> gdome2-xslt

22 years ago...
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 12:03:12 +0000 (12:03 +0000)]
...

22 years ago* Many improvements (expecially in exceptions handling)
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:37:40 +0000 (10:37 +0000)]
* Many improvements (expecially in exceptions handling)
* The cases in which existential variables are now handled "correctly"
  have been increased. Neverthless, existential variables are still implemented
  in a completely wrong way.
* First commit after the commit of cic_unification.

22 years agoOld and dead code from the previous implementation removed.
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:34:57 +0000 (10:34 +0000)]
Old and dead code from the previous implementation removed.

22 years agoFirst (very bugged) version of cic_unification committed.
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:33:28 +0000 (10:33 +0000)]
First (very bugged) version of cic_unification committed.

22 years agoBug fixed in type_of_aux (Cast case).
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:31:06 +0000 (10:31 +0000)]
Bug fixed in type_of_aux (Cast case).

22 years agoGrammar factorized to avoid shift/reduced conflicts that were handled in
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:29:51 +0000 (10:29 +0000)]
Grammar factorized to avoid shift/reduced conflicts that were handled in
the wrong way. No more conflicts left.

22 years ago'-' no more allowed in identifiers
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:28:49 +0000 (10:28 +0000)]
'-' no more allowed in identifiers

22 years ago* New implementation of Apply and Elim based on the latest implementation
Claudio Sacerdoti Coen [Wed, 24 Apr 2002 17:07:57 +0000 (17:07 +0000)]
* New implementation of Apply and Elim based on the latest implementation
  of the unification (not yet commited)

22 years agoModified Files:
Irene Schena [Wed, 24 Apr 2002 16:50:29 +0000 (16:50 +0000)]
Modified Files:
1) grammar.txt: changes
Added Files:
1) query.xml: query example
2) xmathql.dtd: dtd for mathql

22 years agoModified Files:
Irene Schena [Tue, 23 Apr 2002 14:58:22 +0000 (14:58 +0000)]
Modified Files:
1) grammar.txt: added new entries.

22 years ago* The interface of CicTypeChecker now allows the usage of definitions in
Claudio Sacerdoti Coen [Fri, 19 Apr 2002 16:54:59 +0000 (16:54 +0000)]
* The interface of CicTypeChecker now allows the usage of definitions in
  contexts.
* Let...In tactic implemented (but not tested!)

22 years ago* env renamed to context everywhere in cicTypeChecker.ml
Claudio Sacerdoti Coen [Fri, 19 Apr 2002 16:53:48 +0000 (16:53 +0000)]
* env renamed to context everywhere in cicTypeChecker.ml
* Definitions should be allowed in the contexts as well as Declarations.
  This is the very first step: the notion of context is introduced in cic.ml
  and the interface of cicTypeChecker.mli reflects that. (Of course, also the
  interface of cicReduction should do the same!)
  The new implementation just raises an exception when a definition is found
  in the context.

22 years agoAdded Files:
Irene Schena [Fri, 19 Apr 2002 15:38:22 +0000 (15:38 +0000)]
Added Files:
1) grammar.txt: grammar of the Mathematical Query Language

22 years agoBug fixed: reduction in the scratch window now works even if there is no
Claudio Sacerdoti Coen [Fri, 19 Apr 2002 13:03:44 +0000 (13:03 +0000)]
Bug fixed: reduction in the scratch window now works even if there is no
proof in progress.

22 years agoReduction tactics in the scratch window implemented.
Claudio Sacerdoti Coen [Fri, 19 Apr 2002 11:13:49 +0000 (11:13 +0000)]
Reduction tactics in the scratch window implemented.
NOTE: if you select an hypothesis and you apply a reduction tactic, nothing
 will happen and no error message will be reported!

22 years agoDebugging stuff removed.
Claudio Sacerdoti Coen [Fri, 19 Apr 2002 11:12:29 +0000 (11:12 +0000)]
Debugging stuff removed.

22 years agoScratch window is now also raised (= hide + show ;-| when updated.
Claudio Sacerdoti Coen [Thu, 18 Apr 2002 17:03:22 +0000 (17:03 +0000)]
Scratch window is now also raised (= hide + show ;-| when updated.

22 years ago* Error reporting improved
Claudio Sacerdoti Coen [Thu, 18 Apr 2002 15:16:33 +0000 (15:16 +0000)]
* Error reporting improved
* Check now also works when no current goal and/or no current proof is
  available.

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.