]>
matita.cs.unibo.it Git - helm.git/log
Stefano Zacchiroli [Fri, 5 Sep 2003 16:22:09 +0000 (16:22 +0000)]
added \neqt macro
Stefano Zacchiroli [Fri, 5 Sep 2003 16:18:53 +0000 (16:18 +0000)]
added notation for Ropp and Rinv
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 15:39:28 +0000 (15:39 +0000)]
string ==> id
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.
Stefano Zacchiroli [Fri, 5 Sep 2003 15:34:43 +0000 (15:34 +0000)]
fixed associativity of some (all!) binary operators
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 14:31:16 +0000 (14:31 +0000)]
Replace is now working also over Type.
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).
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 12:34:07 +0000 (12:34 +0000)]
Notation for Rdiv and Rminus.
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 10:59:02 +0000 (10:59 +0000)]
Debugging infos removed.
Claudio Sacerdoti Coen [Fri, 5 Sep 2003 10:29:52 +0000 (10:29 +0000)]
string => id
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.
Stefano Zacchiroli [Fri, 5 Sep 2003 08:51:56 +0000 (08:51 +0000)]
replaced with my generic latex makefile
Luca Padovani [Thu, 4 Sep 2003 19:32:38 +0000 (19:32 +0000)]
* update with some candidate methods
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
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_
Stefano Zacchiroli [Thu, 4 Sep 2003 16:46:03 +0000 (16:46 +0000)]
start tutors with nice at the lowest priority
Stefano Zacchiroli [Thu, 4 Sep 2003 16:45:44 +0000 (16:45 +0000)]
avoid deletion of useful .cmi with .PRECIOUS
Stefano Zacchiroli [Thu, 4 Sep 2003 16:45:25 +0000 (16:45 +0000)]
commented out debugging tutor "wait"
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
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
Stefano Zacchiroli [Thu, 4 Sep 2003 16:42:13 +0000 (16:42 +0000)]
added support for X11 clipboard pasting with CTRL-V shortcut
Stefano Zacchiroli [Thu, 4 Sep 2003 16:41:38 +0000 (16:41 +0000)]
added methods to start/stop web services
Stefano Zacchiroli [Thu, 4 Sep 2003 16:41:14 +0000 (16:41 +0000)]
added eqT's macro
pmasoudi [Thu, 4 Sep 2003 15:05:48 +0000 (15:05 +0000)]
scrollbars added & control structure screated
Stefano Zacchiroli [Thu, 4 Sep 2003 15:02:03 +0000 (15:02 +0000)]
fixed typo in eqT's URI
Ferruccio Guidi [Thu, 4 Sep 2003 13:07:26 +0000 (13:07 +0000)]
CGLocateInductive patched
Ferruccio Guidi [Thu, 4 Sep 2003 11:04:15 +0000 (11:04 +0000)]
added the support for the "Locate Inductive Principles" query
Luca Padovani [Fri, 1 Aug 2003 15:32:17 +0000 (15:32 +0000)]
* removed wrong unref
Luca Padovani [Fri, 1 Aug 2003 10:31:22 +0000 (10:31 +0000)]
* added test .html file for mozilla plugin
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
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.
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)
Claudio Sacerdoti Coen [Thu, 31 Jul 2003 14:44:25 +0000 (14:44 +0000)]
"proof of X" closed mactions were not 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
Luca Padovani [Wed, 30 Jul 2003 17:45:58 +0000 (17:45 +0000)]
* mime type updated
Ferruccio Guidi [Wed, 30 Jul 2003 15:45:03 +0000 (15:45 +0000)]
- support for comments added in mathql_db_map.txt
Claudio Sacerdoti Coen [Wed, 30 Jul 2003 15:43:30 +0000 (15:43 +0000)]
Unuseful id removed from hypothesis.
Ferruccio Guidi [Wed, 30 Jul 2003 15:29:52 +0000 (15:29 +0000)]
- information about the database map added in whatsnew.html
- spell checked
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).
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).
Luca Padovani [Tue, 29 Jul 2003 20:04:50 +0000 (20:04 +0000)]
* quite a lot of patches in the building stuff
Ferruccio Guidi [Tue, 29 Jul 2003 16:37:27 +0000 (16:37 +0000)]
new links added
Andrea Asperti [Tue, 29 Jul 2003 14:59:48 +0000 (14:59 +0000)]
Added method FalseInd
Andrea Asperti [Tue, 29 Jul 2003 14:59:08 +0000 (14:59 +0000)]
Added method "FalseInd".
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
...
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
Claudio Sacerdoti Coen [Tue, 29 Jul 2003 11:25:36 +0000 (11:25 +0000)]
Spurious files removed.
Claudio Sacerdoti Coen [Tue, 29 Jul 2003 10:55:47 +0000 (10:55 +0000)]
"(" moved from Mtext to Mo. Spaces removed.
Andrea Asperti [Tue, 29 Jul 2003 09:53:53 +0000 (09:53 +0000)]
Added method AndInd.
Andrea Asperti [Mon, 28 Jul 2003 15:43:35 +0000 (15:43 +0000)]
Added Method "exists".
Andrea Asperti [Mon, 28 Jul 2003 15:42:19 +0000 (15:42 +0000)]
Few modif in eta-fixing.
Claudio Sacerdoti Coen [Mon, 28 Jul 2003 15:21:46 +0000 (15:21 +0000)]
Missing xref for conjectures.
Claudio Sacerdoti Coen [Mon, 28 Jul 2003 15:21:24 +0000 (15:21 +0000)]
mathvariant=normal for all the proof ;-)
Claudio Sacerdoti Coen [Mon, 28 Jul 2003 15:15:58 +0000 (15:15 +0000)]
background (deprecated) ==> mathbackground
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.
Stefano Zacchiroli [Mon, 28 Jul 2003 12:57:10 +0000 (12:57 +0000)]
use OCAMLFIND variable instead of "ocamlfind" directly
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]
Claudio Sacerdoti Coen [Fri, 25 Jul 2003 15:19:02 +0000 (15:19 +0000)]
Highlighting of changed parts.
Claudio Sacerdoti Coen [Fri, 25 Jul 2003 12:31:42 +0000 (12:31 +0000)]
URIs of inductive types and constructors fixed.
Claudio Sacerdoti Coen [Fri, 25 Jul 2003 11:14:42 +0000 (11:14 +0000)]
Lemma generated wrong URIs (again). Fixed.
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.
Andrea Asperti [Thu, 24 Jul 2003 14:05:14 +0000 (14:05 +0000)]
Exact handled in a better way (no more "NO PROOFS").
Andrea Asperti [Thu, 24 Jul 2003 13:19:20 +0000 (13:19 +0000)]
The name of TD proofs was erroneously always set to previous.
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.
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
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
Andrea Asperti [Tue, 22 Jul 2003 15:51:33 +0000 (15:51 +0000)]
Debugging stuff changed.
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!
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.
Andrea Asperti [Tue, 22 Jul 2003 15:11:55 +0000 (15:11 +0000)]
Previous commit was erroneous and dit not compile.
Fixed.
Claudio Sacerdoti Coen [Tue, 22 Jul 2003 14:29:16 +0000 (14:29 +0000)]
Debugging code inserted bug in the code ;-)
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.
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?
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.
Claudio Sacerdoti Coen [Mon, 21 Jul 2003 14:06:17 +0000 (14:06 +0000)]
Interface change: only cobj2obj is exposed.
Claudio Sacerdoti Coen [Mon, 21 Jul 2003 14:01:58 +0000 (14:01 +0000)]
Flattening application contexts uncorrectly changed the proof ids.
Andrea Asperti [Mon, 21 Jul 2003 12:10:58 +0000 (12:10 +0000)]
** UNTESTED **
Fix and CoFix are now handled "correctly" ;-)
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).
Andrea Asperti [Mon, 21 Jul 2003 10:19:23 +0000 (10:19 +0000)]
Rendering of current proofs completed.
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 16:02:49 +0000 (16:02 +0000)]
Reindenting.
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.
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 15:53:57 +0000 (15:53 +0000)]
Cic2acic is now responsible of eta-fixing the objects.
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).
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 15:37:04 +0000 (15:37 +0000)]
cic2content.ml* moved from cic_transformations 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.
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 13:05:44 +0000 (13:05 +0000)]
...
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 11:23:58 +0000 (11:23 +0000)]
cic_transformations factorized into cic_omdoc and cic_transformations.
Claudio Sacerdoti Coen [Sun, 20 Jul 2003 11:05:12 +0000 (11:05 +0000)]
Cic2content split into Content and Cic2content.
Andrea Asperti [Fri, 18 Jul 2003 18:01:29 +0000 (18:01 +0000)]
CSC: tentative definition of the ocaml structure that represents
OMDoc objects.
Ferruccio Guidi [Thu, 17 Jul 2003 22:03:59 +0000 (22:03 +0000)]
some documentation added
pmasoudi [Thu, 17 Jul 2003 14:23:29 +0000 (14:23 +0000)]
Partional first fase final.
Ferruccio Guidi [Thu, 17 Jul 2003 14:02:53 +0000 (14:02 +0000)]
dead code removed
pmasoudi [Thu, 17 Jul 2003 12:52:47 +0000 (12:52 +0000)]
Persist file completed.
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
Luca Padovani [Thu, 17 Jul 2003 10:28:06 +0000 (10:28 +0000)]
* changed name of shared library
Luca Padovani [Thu, 17 Jul 2003 10:23:52 +0000 (10:23 +0000)]
* snapshot
Luca Padovani [Thu, 17 Jul 2003 10:23:24 +0000 (10:23 +0000)]
* added simple test program
Luca Padovani [Thu, 17 Jul 2003 10:22:38 +0000 (10:22 +0000)]
* the container seems to work now
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).
pmasoudi [Wed, 16 Jul 2003 17:33:09 +0000 (17:33 +0000)]
Control Factory modified.