]> matita.cs.unibo.it Git - helm.git/log
helm.git
21 years agoadded "start" and "stop" targets for hbugs
Stefano Zacchiroli [Sun, 7 Sep 2003 09:50:29 +0000 (09:50 +0000)]
added "start" and "stop" targets for hbugs

21 years agoadded support for external configuration of describe_hint_callback
Stefano Zacchiroli [Sun, 7 Sep 2003 09:50:09 +0000 (09:50 +0000)]
added support for external configuration of describe_hint_callback

21 years agoadded "describe_hint_callback" invoked when a hint is selected
Stefano Zacchiroli [Sun, 7 Sep 2003 09:49:07 +0000 (09:49 +0000)]
added "describe_hint_callback" invoked when a hint is selected

21 years ago- removed useless status bar
Stefano Zacchiroli [Sun, 7 Sep 2003 09:48:27 +0000 (09:48 +0000)]
- removed useless status bar
- hid menu bar
- added (Re)Register button
- added vertical pane between subscription and hints
- changed default size to a "decent"-one

21 years agosend SIGKILL to stop web services
Stefano Zacchiroli [Sun, 7 Sep 2003 09:47:03 +0000 (09:47 +0000)]
send SIGKILL to stop web services

21 years agocommented out thread killing (we have to wait for a decent Thread.exit
Stefano Zacchiroli [Sun, 7 Sep 2003 09:46:14 +0000 (09:46 +0000)]
commented out thread killing (we have to wait for a decent Thread.exit
implementation)

21 years agoget_childNodes no longer used ==> major performance speed-up
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 17:33:04 +0000 (17:33 +0000)]
get_childNodes no longer used ==> major performance speed-up

21 years agoDefs in context may now have an optional type (when unknown).
Stefano Zacchiroli [Fri, 5 Sep 2003 16:23:17 +0000 (16:23 +0000)]
Defs in context may now have an optional type (when unknown).

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.

21 years agoadded \neqt macro
Stefano Zacchiroli [Fri, 5 Sep 2003 16:22:09 +0000 (16:22 +0000)]
added \neqt macro

21 years agoadded notation for Ropp and Rinv
Stefano Zacchiroli [Fri, 5 Sep 2003 16:18:53 +0000 (16:18 +0000)]
added notation for Ropp and Rinv

21 years agostring ==> id
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 15:39:28 +0000 (15:39 +0000)]
string ==> id

21 years agoDefs in context may now have an optional type (when unknown).
Stefano Zacchiroli [Fri, 5 Sep 2003 15:36:28 +0000 (15:36 +0000)]
Defs in context may now have an optional type (when unknown).

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.

21 years agofixed associativity of some (all!) binary operators
Stefano Zacchiroli [Fri, 5 Sep 2003 15:34:43 +0000 (15:34 +0000)]
fixed associativity of some (all!) binary operators

21 years agoReplace is now working also over Type.
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 14:31:16 +0000 (14:31 +0000)]
Replace is now working also over Type.

21 years agoReplace tactic fixed. It was not working any longer. (It produced a dummy
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 13:00:27 +0000 (13:00 +0000)]
Replace tactic fixed. It was not working any longer. (It produced a dummy
eta-expansion).

21 years agoNotation for Rdiv and Rminus.
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 12:34:07 +0000 (12:34 +0000)]
Notation for Rdiv and Rminus.

21 years agoDebugging infos removed.
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 10:59:02 +0000 (10:59 +0000)]
Debugging infos removed.

21 years agostring => id
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 10:29:52 +0000 (10:29 +0000)]
string => id

21 years agoDefs in context may now have an optional type (when unknown).
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 10:29:13 +0000 (10:29 +0000)]
Defs in context may now have an optional type (when unknown).

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.

21 years agoreplaced with my generic latex makefile
Stefano Zacchiroli [Fri, 5 Sep 2003 08:51:56 +0000 (08:51 +0000)]
replaced with my generic latex makefile

21 years ago* update with some candidate methods
Luca Padovani [Thu, 4 Sep 2003 19:32:38 +0000 (19:32 +0000)]
* update with some candidate methods

21 years ago* added test View interface. It is basically empty but eventually it will host
Luca Padovani [Thu, 4 Sep 2003 18:46:14 +0000 (18:46 +0000)]
* added test View interface. It is basically empty but eventually it will host
  any gtkmathview-specific method

21 years ago- added a destroy callback
Stefano Zacchiroli [Thu, 4 Sep 2003 16:46:46 +0000 (16:46 +0000)]
- added a destroy callback
- ignore delete events on hbugs window
- unsubscribe only when hbugs window gets _destroyed_

21 years agostart tutors with nice at the lowest priority
Stefano Zacchiroli [Thu, 4 Sep 2003 16:46:03 +0000 (16:46 +0000)]
start tutors with nice at the lowest priority

21 years agoavoid deletion of useful .cmi with .PRECIOUS
Stefano Zacchiroli [Thu, 4 Sep 2003 16:45:44 +0000 (16:45 +0000)]
avoid deletion of useful .cmi with .PRECIOUS

21 years agocommented out debugging tutor "wait"
Stefano Zacchiroli [Thu, 4 Sep 2003 16:45:25 +0000 (16:45 +0000)]
commented out debugging tutor "wait"

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