]> matita.cs.unibo.it Git - helm.git/log
helm.git
21 years ago- added dot notation for real numbers and basic operations on them
Stefano Zacchiroli [Thu, 4 Sep 2003 16:44:04 +0000 (16:44 +0000)]
- added dot notation for real numbers and basic operations on them
- added support for \eqt

21 years ago- added default URI for new theorems
Stefano Zacchiroli [Thu, 4 Sep 2003 16:43:25 +0000 (16:43 +0000)]
- added default URI for new theorems
- added menu items to the hbugs menu for:
  * start and stop hbugs web services
  * force submission of current status

21 years agoadded support for X11 clipboard pasting with CTRL-V shortcut
Stefano Zacchiroli [Thu, 4 Sep 2003 16:42:13 +0000 (16:42 +0000)]
added support for X11 clipboard pasting with CTRL-V shortcut

21 years agoadded methods to start/stop web services
Stefano Zacchiroli [Thu, 4 Sep 2003 16:41:38 +0000 (16:41 +0000)]
added methods to start/stop web services

21 years agoadded eqT's macro
Stefano Zacchiroli [Thu, 4 Sep 2003 16:41:14 +0000 (16:41 +0000)]
added eqT's macro

21 years agoscrollbars added & control structure screated
pmasoudi [Thu, 4 Sep 2003 15:05:48 +0000 (15:05 +0000)]
scrollbars added & control structure screated

21 years agofixed typo in eqT's URI
Stefano Zacchiroli [Thu, 4 Sep 2003 15:02:03 +0000 (15:02 +0000)]
fixed typo in eqT's URI

21 years agoCGLocateInductive patched
Ferruccio Guidi [Thu, 4 Sep 2003 13:07:26 +0000 (13:07 +0000)]
CGLocateInductive patched

21 years agoadded the support for the "Locate Inductive Principles" query
Ferruccio Guidi [Thu, 4 Sep 2003 11:04:15 +0000 (11:04 +0000)]
added the support for the "Locate Inductive Principles" query

21 years ago* removed wrong unref
Luca Padovani [Fri, 1 Aug 2003 15:32:17 +0000 (15:32 +0000)]
* removed wrong unref

21 years ago* added test .html file for mozilla plugin
Luca Padovani [Fri, 1 Aug 2003 10:31:22 +0000 (10:31 +0000)]
* added test .html file for mozilla plugin

21 years ago* a few adjustments and debugging messages added
Luca Padovani [Fri, 1 Aug 2003 10:15:57 +0000 (10:15 +0000)]
* a few adjustments and debugging messages added
* works as a component in mozilla

21 years agoClosed induction cases are now pointers to the acontext/conclusion ==>
Claudio Sacerdoti Coen [Thu, 31 Jul 2003 15:41:05 +0000 (15:41 +0000)]
Closed induction cases are now pointers to the acontext/conclusion ==>
they are now perforated correctly.

21 years ago* added first version of persist stream implementation (not yet working)
pmasoudi [Thu, 31 Jul 2003 14:54:14 +0000 (14:54 +0000)]
* added first version of persist stream implementation (not yet working)
* added test for property bag (read-only for now)

21 years ago"proof of X" closed mactions were not selectable
Claudio Sacerdoti Coen [Thu, 31 Jul 2003 14:44:25 +0000 (14:44 +0000)]
"proof of X" closed mactions were not selectable

21 years ago1. folded maction are now selectable
Claudio Sacerdoti Coen [Thu, 31 Jul 2003 08:14:43 +0000 (08:14 +0000)]
1. folded maction are now selectable
2. metavariable occurrences are now displayed together with their
   substitution (to be improved)
3. the hypothesis in the metasenv are now displayed in the right order

21 years ago* mime type updated
Luca Padovani [Wed, 30 Jul 2003 17:45:58 +0000 (17:45 +0000)]
* mime type updated

21 years ago- support for comments added in mathql_db_map.txt
Ferruccio Guidi [Wed, 30 Jul 2003 15:45:03 +0000 (15:45 +0000)]
- support for comments added in mathql_db_map.txt

21 years agoUnuseful id removed from hypothesis.
Claudio Sacerdoti Coen [Wed, 30 Jul 2003 15:43:30 +0000 (15:43 +0000)]
Unuseful id removed from hypothesis.

21 years ago- information about the database map added in whatsnew.html
Ferruccio Guidi [Wed, 30 Jul 2003 15:29:52 +0000 (15:29 +0000)]
- information about the database map added in whatsnew.html
- spell checked

21 years agoEta fixing for MTCases added (that meant to recursively pass around the
Andrea Asperti [Wed, 30 Jul 2003 12:58:07 +0000 (12:58 +0000)]
Eta fixing for MTCases added (that meant to recursively pass around the
context).

21 years agoAll the ids are now generated by gen_id. (Some of them were previously based
Claudio Sacerdoti Coen [Wed, 30 Jul 2003 09:26:19 +0000 (09:26 +0000)]
All the ids are now generated by gen_id. (Some of them were previously based
on the acic ids).

21 years ago* quite a lot of patches in the building stuff
Luca Padovani [Tue, 29 Jul 2003 20:04:50 +0000 (20:04 +0000)]
* quite a lot of patches in the building stuff

21 years agonew links added
Ferruccio Guidi [Tue, 29 Jul 2003 16:37:27 +0000 (16:37 +0000)]
new links added

21 years agoAdded method FalseInd
Andrea Asperti [Tue, 29 Jul 2003 14:59:48 +0000 (14:59 +0000)]
Added method FalseInd

21 years agoAdded method "FalseInd".
Andrea Asperti [Tue, 29 Jul 2003 14:59:08 +0000 (14:59 +0000)]
Added method "FalseInd".

21 years agoPrefixes introduced for the generated ids/xrefs. Example:
Claudio Sacerdoti Coen [Tue, 29 Jul 2003 14:44:19 +0000 (14:44 +0000)]
Prefixes introduced for the generated ids/xrefs. Example:
 "proof:" for proofs
 "decl:"  for declarations
 ...

21 years ago- the mathql interpreter is not helm-dependent any more
Ferruccio Guidi [Tue, 29 Jul 2003 11:41:25 +0000 (11:41 +0000)]
- the mathql interpreter is not helm-dependent any more
- fixed a bug in the "match conclusion" query of the search engine
- gTopLevel/Makefile improved

21 years agoSpurious files removed.
Claudio Sacerdoti Coen [Tue, 29 Jul 2003 11:25:36 +0000 (11:25 +0000)]
Spurious files removed.

21 years ago"(" moved from Mtext to Mo. Spaces removed.
Claudio Sacerdoti Coen [Tue, 29 Jul 2003 10:55:47 +0000 (10:55 +0000)]
"(" moved from Mtext to Mo. Spaces removed.

21 years agoAdded method AndInd.
Andrea Asperti [Tue, 29 Jul 2003 09:53:53 +0000 (09:53 +0000)]
Added method AndInd.

21 years agoAdded Method "exists".
Andrea Asperti [Mon, 28 Jul 2003 15:43:35 +0000 (15:43 +0000)]
Added Method "exists".

21 years agoFew modif in eta-fixing.
Andrea Asperti [Mon, 28 Jul 2003 15:42:19 +0000 (15:42 +0000)]
Few modif in eta-fixing.

21 years agoMissing xref for conjectures.
Claudio Sacerdoti Coen [Mon, 28 Jul 2003 15:21:46 +0000 (15:21 +0000)]
Missing xref for conjectures.

21 years agomathvariant=normal for all the proof ;-)
Claudio Sacerdoti Coen [Mon, 28 Jul 2003 15:21:24 +0000 (15:21 +0000)]
mathvariant=normal for all the proof ;-)

21 years agobackground (deprecated) ==> mathbackground
Claudio Sacerdoti Coen [Mon, 28 Jul 2003 15:15:58 +0000 (15:15 +0000)]
background (deprecated) ==> mathbackground

21 years agoBug fixed: it could have happened that the tree structured becomes scrambled
Claudio Sacerdoti Coen [Mon, 28 Jul 2003 13:28:11 +0000 (13:28 +0000)]
Bug fixed: it could have happened that the tree structured becomes scrambled
by the highlighting operation.

21 years agouse OCAMLFIND variable instead of "ocamlfind" directly
Stefano Zacchiroli [Mon, 28 Jul 2003 12:57:10 +0000 (12:57 +0000)]
use OCAMLFIND variable instead of "ocamlfind" directly

21 years ago- severe bug fixing
Claudio Sacerdoti Coen [Mon, 28 Jul 2003 10:55:13 +0000 (10:55 +0000)]
- severe bug fixing
- implementation of two functions to highlight/dim set of nodes given
  their xref. [used to highlight/dim the current goal]

21 years agoHighlighting of changed parts.
Claudio Sacerdoti Coen [Fri, 25 Jul 2003 15:19:02 +0000 (15:19 +0000)]
Highlighting of changed parts.

21 years agoURIs of inductive types and constructors fixed.
Claudio Sacerdoti Coen [Fri, 25 Jul 2003 12:31:42 +0000 (12:31 +0000)]
URIs of inductive types and constructors fixed.

21 years agoLemma generated wrong URIs (again). Fixed.
Claudio Sacerdoti Coen [Fri, 25 Jul 2003 11:14:42 +0000 (11:14 +0000)]
Lemma generated wrong URIs (again). Fixed.

21 years agoComplete beta reduction added to avoid strange case of deep beta-redexes
Andrea Asperti [Thu, 24 Jul 2003 14:06:03 +0000 (14:06 +0000)]
Complete beta reduction added to avoid strange case of deep beta-redexes
in the expected types of application heads.

21 years agoExact handled in a better way (no more "NO PROOFS").
Andrea Asperti [Thu, 24 Jul 2003 14:05:14 +0000 (14:05 +0000)]
Exact handled in a better way (no more "NO PROOFS").

21 years agoThe name of TD proofs was erroneously always set to previous.
Andrea Asperti [Thu, 24 Jul 2003 13:19:20 +0000 (13:19 +0000)]
The name of TD proofs was erroneously always set to previous.

21 years agoImproved management of conclusions, to avoid repetitions.
Andrea Asperti [Thu, 24 Jul 2003 11:40:02 +0000 (11:40 +0000)]
Improved management of conclusions, to avoid repetitions.
Some problems of xrefs have been fixed.

21 years ago- better handling of proof expansion/contraction
Andrea Asperti [Wed, 23 Jul 2003 17:03:33 +0000 (17:03 +0000)]
- better handling of proof expansion/contraction
- helm:xref added in most places

21 years ago- Lemma added to the list of proof arguments
Andrea Asperti [Wed, 23 Jul 2003 17:02:54 +0000 (17:02 +0000)]
- Lemma added to the list of proof arguments
- Lemma used for Const, MutConst and Var in Apply arguments
- atomization of complex proofs is now performed also in tactics different
  from Apply

21 years agoDebugging stuff changed.
Andrea Asperti [Tue, 22 Jul 2003 15:51:33 +0000 (15:51 +0000)]
Debugging stuff changed.

21 years ago"Final" commit that patches termViewer while still enabling XML Diffing.
Andrea Asperti [Tue, 22 Jul 2003 15:51:00 +0000 (15:51 +0000)]
"Final" commit that patches termViewer while still enabling XML Diffing.
Awesome performances!

21 years ago- selection attribute of maction is now explicitly generated
Claudio Sacerdoti Coen [Tue, 22 Jul 2003 15:46:34 +0000 (15:46 +0000)]
- selection attribute of maction is now explicitly generated
- all the conjectures are now put in a table to avoid too many
  changes that make Xml Diffing difficult.

21 years agoPrevious commit was erroneous and dit not compile.
Andrea Asperti [Tue, 22 Jul 2003 15:11:55 +0000 (15:11 +0000)]
Previous commit was erroneous and dit not compile.
Fixed.

21 years agoDebugging code inserted bug in the code ;-)
Claudio Sacerdoti Coen [Tue, 22 Jul 2003 14:29:16 +0000 (14:29 +0000)]
Debugging code inserted bug in the code ;-)

21 years agoXmlDiff-ing of DOM trees implemented.
Claudio Sacerdoti Coen [Tue, 22 Jul 2003 14:08:39 +0000 (14:08 +0000)]
XmlDiff-ing of DOM trees implemented.
SPECIAL FEATURE: the selection attribute of mactions are not patched.

21 years ago1. Modificiations due to the change ot K.Aux
Andrea Asperti [Tue, 22 Jul 2003 08:43:32 +0000 (08:43 +0000)]
1. Modificiations due to the change ot K.Aux
2. Assert false on Lambda with no name removed. Who generates them?

21 years agoThe Aux argument of conclude is now of type string (used to be int).
Andrea Asperti [Mon, 21 Jul 2003 17:03:37 +0000 (17:03 +0000)]
The Aux argument of conclude is now of type string (used to be int).
Case Fixed.

21 years agoInterface change: only cobj2obj is exposed.
Claudio Sacerdoti Coen [Mon, 21 Jul 2003 14:06:17 +0000 (14:06 +0000)]
Interface change: only cobj2obj is exposed.

21 years agoFlattening application contexts uncorrectly changed the proof ids.
Claudio Sacerdoti Coen [Mon, 21 Jul 2003 14:01:58 +0000 (14:01 +0000)]
Flattening application contexts uncorrectly changed the proof ids.

21 years ago** UNTESTED **
Andrea Asperti [Mon, 21 Jul 2003 12:10:58 +0000 (12:10 +0000)]
** UNTESTED **
Fix and CoFix are now handled "correctly" ;-)

21 years agoWe do not compute inner-types for the metasenv ==> we handle it in a particular
Andrea Asperti [Mon, 21 Jul 2003 10:34:39 +0000 (10:34 +0000)]
We do not compute inner-types for the metasenv ==> we handle it in a particular
way, always generating `Declaration and `Definition (instead of `Hypothesis and
`Proof when the sort is Prop).

21 years agoRendering of current proofs completed.
Andrea Asperti [Mon, 21 Jul 2003 10:19:23 +0000 (10:19 +0000)]
Rendering of current proofs completed.

21 years agoReindenting.
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 16:02:49 +0000 (16:02 +0000)]
Reindenting.

21 years agoproof2cic now uses Deannotate.deannoate_term instead of having an input
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 15:58:58 +0000 (15:58 +0000)]
proof2cic now uses Deannotate.deannoate_term instead of having an input
parameter.

21 years agoCic2acic is now responsible of eta-fixing the objects.
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 15:53:57 +0000 (15:53 +0000)]
Cic2acic is now responsible of eta-fixing the objects.

21 years agoCic2acic is now responsible of eta-fixing the objects (using the Eta_fix
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 15:53:12 +0000 (15:53 +0000)]
Cic2acic is now responsible of eta-fixing the objects (using the Eta_fix
module).

21 years agocic2content.ml* moved from cic_transformations to cic_omdoc.
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 15:37:04 +0000 (15:37 +0000)]
cic2content.ml* moved from cic_transformations to cic_omdoc.

21 years agoContent2cic e Eta_fixing moved from gTopLevel to cic_omdoc.
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 13:08:25 +0000 (13:08 +0000)]
Content2cic e Eta_fixing moved from gTopLevel to cic_omdoc.

21 years ago...
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 13:05:44 +0000 (13:05 +0000)]
...

21 years agocic_transformations factorized into cic_omdoc and cic_transformations.
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 11:23:58 +0000 (11:23 +0000)]
cic_transformations factorized into cic_omdoc and cic_transformations.

21 years agoCic2content split into Content and Cic2content.
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 11:05:12 +0000 (11:05 +0000)]
Cic2content split into Content and Cic2content.

21 years agoCSC: tentative definition of the ocaml structure that represents
Andrea Asperti [Fri, 18 Jul 2003 18:01:29 +0000 (18:01 +0000)]
CSC: tentative definition of the ocaml structure that represents
 OMDoc objects.

21 years agosome documentation added
Ferruccio Guidi [Thu, 17 Jul 2003 22:03:59 +0000 (22:03 +0000)]
some documentation added

21 years agoPartional first fase final.
pmasoudi [Thu, 17 Jul 2003 14:23:29 +0000 (14:23 +0000)]
Partional first fase final.

21 years agodead code removed
Ferruccio Guidi [Thu, 17 Jul 2003 14:02:53 +0000 (14:02 +0000)]
dead code removed

21 years agoPersist file completed.
pmasoudi [Thu, 17 Jul 2003 12:52:47 +0000 (12:52 +0000)]
Persist file completed.

21 years ago- new generated query "unreferred" implemented at server side
Ferruccio Guidi [Thu, 17 Jul 2003 12:30:26 +0000 (12:30 +0000)]
- new generated query "unreferred" implemented at server side
- fixed some aspects of the constraint generator for "matchConclusion"
- fixed a bug that prevented to "make opt" in ocaml/gTopLevel

21 years ago* changed name of shared library
Luca Padovani [Thu, 17 Jul 2003 10:28:06 +0000 (10:28 +0000)]
* changed name of shared library

21 years ago* snapshot
Luca Padovani [Thu, 17 Jul 2003 10:23:52 +0000 (10:23 +0000)]
* snapshot

21 years ago* added simple test program
Luca Padovani [Thu, 17 Jul 2003 10:23:24 +0000 (10:23 +0000)]
* added simple test program

21 years ago* the container seems to work now
Luca Padovani [Thu, 17 Jul 2003 10:22:38 +0000 (10:22 +0000)]
* the container seems to work now

21 years agoXml.token is now namespace-aware. As a consequence, xml2Gdomexmath is
Claudio Sacerdoti Coen [Wed, 16 Jul 2003 22:46:22 +0000 (22:46 +0000)]
Xml.token is now namespace-aware. As a consequence, xml2Gdomexmath is
no longer needed. (It was a terrible hack indeed).

21 years agoControl Factory modified.
pmasoudi [Wed, 16 Jul 2003 17:33:09 +0000 (17:33 +0000)]
Control Factory modified.

21 years agopersist file with factory.
pmasoudi [Wed, 16 Jul 2003 16:13:29 +0000 (16:13 +0000)]
persist file with factory.

21 years agoSeveral changes (the beginning of a new era???)
Andrea Asperti [Wed, 16 Jul 2003 14:12:02 +0000 (14:12 +0000)]
Several changes (the beginning of a new era???)
 1. stuff related to transformations (stylesheets and so on)
    moved from gTopLevel to the new library cic_transformations
 2. porting of the stylesheets to old plain ocaml code by Andrea Asperti.
    Also in cic_transformations.

Disclaimer:
 A. the ocaml transformations are still incomplete and under development.
    They are a bit more performant, though. (just a few order of magnitudes)
 B. the cic_transformation library seems a bit of a mess right now.
    Much clean-up needed.

21 years agoadded persit-file-implementation.
pmasoudi [Wed, 16 Jul 2003 12:48:25 +0000 (12:48 +0000)]
added persit-file-implementation.

21 years ago* changed name to control factory
Luca Padovani [Wed, 16 Jul 2003 12:46:11 +0000 (12:46 +0000)]
* changed name to control factory

21 years ago* updated the help file to reflect the new syntax (reload/remove)
Luca Padovani [Wed, 16 Jul 2003 08:45:34 +0000 (08:45 +0000)]
* updated the help file to reflect the new syntax (reload/remove)

21 years ago* syntax update for "remove all stylesheets" in control.js
Luca Padovani [Wed, 16 Jul 2003 08:39:41 +0000 (08:39 +0000)]
* syntax update for "remove all stylesheets" in control.js
* reloadAll function created

21 years ago* added .pc file
Luca Padovani [Tue, 15 Jul 2003 17:45:16 +0000 (17:45 +0000)]
* added .pc file
* IDL interface version computed from package version

21 years agoCamera ready.
Claudio Sacerdoti Coen [Tue, 15 Jul 2003 16:02:25 +0000 (16:02 +0000)]
Camera ready.

21 years ago* substituting the right version variable
Luca Padovani [Tue, 15 Jul 2003 15:06:30 +0000 (15:06 +0000)]
* substituting the right version variable

21 years ago* wrong variable for version
Luca Padovani [Tue, 15 Jul 2003 15:05:28 +0000 (15:05 +0000)]
* wrong variable for version

21 years ago* patched version of shared library
Luca Padovani [Tue, 15 Jul 2003 15:03:27 +0000 (15:03 +0000)]
* patched version of shared library

21 years ago* first snapshot
Luca Padovani [Tue, 15 Jul 2003 14:54:22 +0000 (14:54 +0000)]
* first snapshot

21 years agomerged CSC's typos squashing
Stefano Zacchiroli [Tue, 15 Jul 2003 14:50:42 +0000 (14:50 +0000)]
merged CSC's typos squashing

21 years agofixed "s" typos
Stefano Zacchiroli [Tue, 15 Jul 2003 10:14:24 +0000 (10:14 +0000)]
fixed "s" typos

21 years agodescription for "Irene Schena" added in authors.html
Ferruccio Guidi [Tue, 15 Jul 2003 09:17:59 +0000 (09:17 +0000)]
description for "Irene Schena" added in authors.html

21 years agowrapped libxslt stylesheet application inside an ocaml blocking section
Stefano Zacchiroli [Tue, 15 Jul 2003 06:36:25 +0000 (06:36 +0000)]
wrapped libxslt stylesheet application inside an ocaml blocking section
so that ocaml exceptions, signals and other asynchronous stuff could be
handled in the meantime

21 years agobumped version to 0.0.5
Stefano Zacchiroli [Tue, 15 Jul 2003 06:35:42 +0000 (06:35 +0000)]
bumped version to 0.0.5

21 years agoTowards the camera ready.
Claudio Sacerdoti Coen [Mon, 14 Jul 2003 17:05:15 +0000 (17:05 +0000)]
Towards the camera ready.