matita.cs.unibo.it Git - helm.git/history - helm/gTopLevel/gTopLevel.ml

]> matita.cs.unibo.it Git - helm.git/history - helm/gTopLevel/gTopLevel.ml

[helm.git] / helm / gTopLevel / gTopLevel.ml

2005-02-07	Enrico Tassi	sync with Xml.pp	blob \| commitdiff \| raw
2005-02-03	Enrico Tassi	removed uri parameter from load_proof	blob \| commitdiff \| raw \| diff to current
2005-01-21	Enrico Tassi	- sync with the new ApplyTransformation API	blob \| commitdiff \| raw \| diff to current
2005-01-20	Stefano Zacchiroli	helmns -> helm_ns	blob \| commitdiff \| raw \| diff to current
2005-01-17	Enrico Tassi	new cicEnvironment implementation	blob \| commitdiff \| raw \| diff to current
2004-12-01	Enrico Tassi	Added universes handling. Tag PRE_UNIVERSES may help ;)	blob \| commitdiff \| raw \| diff to current
2004-11-29	Stefano Zacchiroli	- passes subst to FreshNameGenerator	blob \| commitdiff \| raw \| diff to current
2004-11-03	Stefano Zacchiroli	no longer use Dbi module but directly use Mysql module...	blob \| commitdiff \| raw \| diff to current
2004-10-22	Stefano Zacchiroli	- support also DBI handle	blob \| commitdiff \| raw \| diff to current
2004-10-14	Claudio Sacerdoti...	Luca (bugged) debugging stuff removed.	blob \| commitdiff \| raw \| diff to current
2004-09-28	Luca Padovani	* minor correction to make the new mathml widget work...	blob \| commitdiff \| raw \| diff to current
2004-09-09	Ferruccio Guidi	now should run also when the db is down (untested)	blob \| commitdiff \| raw \| diff to current
2004-09-09	Stefano Zacchiroli	ported to latest lablgtkmathview	blob \| commitdiff \| raw \| diff to current
2004-06-01	Enrico Tassi	new universes implementation	blob \| commitdiff \| raw \| diff to current
2004-05-13	Ferruccio Guidi	- some code patched	blob \| commitdiff \| raw \| diff to current
2004-05-13	Stefano Zacchiroli	changed proofStatus so that uri component is optional...	blob \| commitdiff \| raw \| diff to current
2004-04-29	Stefano Zacchiroli	- moved applyTransformation initialization code to...	blob \| commitdiff \| raw \| diff to current
2004-04-28	Stefano Zacchiroli	added extra "id" parameter for input_or_locate_uri...	blob \| commitdiff \| raw \| diff to current
2004-04-20	Stefano Zacchiroli	got rid of a ~status label	blob \| commitdiff \| raw \| diff to current
2004-03-12	acerioni	New tactic Auto.	blob \| commitdiff \| raw \| diff to current
2004-03-02	Claudio Sacerdoti...	The disambiguation now returns a list of interpretations.	blob \| commitdiff \| raw \| diff to current
2004-02-20	Ferruccio Guidi	- mathql interpreter flags reorganized	blob \| commitdiff \| raw \| diff to current
2004-02-18	Ferruccio Guidi	mathql interpreter flags can be now red from helm registry	blob \| commitdiff \| raw \| diff to current
2004-02-17	Claudio Sacerdoti...	mathql_db_map.txt is now retrieved by Helm_registry.	blob \| commitdiff \| raw \| diff to current
2004-02-17	Claudio Sacerdoti...	triciclo.conf.xml ==> gTopLevel.conf.xml	blob \| commitdiff \| raw \| diff to current
2004-02-16	Claudio Sacerdoti...	- triciclo.conf.xml.sample ported to the latest version...	blob \| commitdiff \| raw \| diff to current
2004-02-11	Stefano Zacchiroli	bugfix: auto_disambiguation is not considered for searc...	blob \| commitdiff \| raw \| diff to current
2004-02-11	Stefano Zacchiroli	new getter, logger, and the hell	blob \| commitdiff \| raw \| diff to current
2004-02-09	Claudio Sacerdoti...	Added flag ?eta_fix:bool to acic_object_of_cic_object.	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	fresh_name_generator has now also the metasenv parameter.	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	mk_fresh_name moved to FreshNamesGenerator.	blob \| commitdiff \| raw \| diff to current
2004-01-30	Stefano Zacchiroli	s/Callbacks/DisambiguateCallbacks/	blob \| commitdiff \| raw \| diff to current
2004-01-29	Stefano Zacchiroli	- s/TexTermEditor/TermEditor/ (* former no longer appro...	blob \| commitdiff \| raw \| diff to current
2004-01-29	Stefano Zacchiroli	- added "clear alias" menu item	blob \| commitdiff \| raw \| diff to current
2004-01-24	Stefano Zacchiroli	- s/id_to_uris/environment/	blob \| commitdiff \| raw \| diff to current
2004-01-24	Stefano Zacchiroli	- quiet debugging for mathql	blob \| commitdiff \| raw \| diff to current
2004-01-23	Stefano Zacchiroli	moved environmentP3 in cic_textual_parser2 and reshaped...	blob \| commitdiff \| raw \| diff to current
2004-01-23	Claudio Sacerdoti...	- Added DisambiguatingParser (that abstracts both the...	blob \| commitdiff \| raw \| diff to current
2004-01-22	Stefano Zacchiroli	(temporary, waiting for abstraction over disambiguators...	blob \| commitdiff \| raw \| diff to current
2003-12-16	Stefano Zacchiroli	- fixed logging in log window so that spurious html...	blob \| commitdiff \| raw \| diff to current
2003-12-02	Ferruccio Guidi	sort CProp added	blob \| commitdiff \| raw \| diff to current
2003-11-06	Claudio Sacerdoti...	HBugs compile again (but it does not do anything right...	blob \| commitdiff \| raw \| diff to current
2003-11-04	Luca Padovani	* first upgrade to the new error logging mechanism	blob \| commitdiff \| raw \| diff to current
2003-10-29	Ferruccio Guidi	some interfaces changed to prepare the mathql code...	blob \| commitdiff \| raw \| diff to current
2003-10-29	Luca Padovani	* updated for gtk2	blob \| commitdiff \| raw \| diff to current
2003-09-23	Claudio Sacerdoti...	Reindentation.	blob \| commitdiff \| raw \| diff to current
2003-09-23	Claudio Sacerdoti...	ProofEngine.goal := ==> set_proof_engine_goal	blob \| commitdiff \| raw \| diff to current
2003-09-23	Claudio Sacerdoti...	Reindentation	blob \| commitdiff \| raw \| diff to current
2003-09-23	Claudio Sacerdoti...	ProofEngine.proof is now an abstract data type (since...	blob \| commitdiff \| raw \| diff to current
2003-09-14	Stefano Zacchiroli	- bumped copyright years	blob \| commitdiff \| raw \| diff to current
2003-09-07	Stefano Zacchiroli	- use hbugs' describe_callback to render apply-hints...	blob \| commitdiff \| raw \| diff to current
2003-09-04	Stefano Zacchiroli	- added default URI for new theorems	blob \| commitdiff \| raw \| diff to current
2003-09-04	Ferruccio Guidi	added the support for the "Locate Inductive Principles...	blob \| commitdiff \| raw \| diff to current
2003-07-20	Claudio Sacerdoti...	Cic2acic is now responsible of eta-fixing the objects.	blob \| commitdiff \| raw \| diff to current
2003-07-17	Ferruccio Guidi	- new generated query "unreferred" implemented at serve...	blob \| commitdiff \| raw \| diff to current
2003-07-16	Andrea Asperti	Several changes (the beginning of a new era???)	blob \| commitdiff \| raw \| diff to current
2003-07-02	Ferruccio Guidi	mathql_generator: new constraint format (more type...	blob \| commitdiff \| raw \| diff to current
2003-06-30	Claudio Sacerdoti...	- default font size of the proof window lowered to 10	blob \| commitdiff \| raw \| diff to current
2003-06-27	Claudio Sacerdoti...	The "Save proof" menu item is now activated when a...	blob \| commitdiff \| raw \| diff to current
2003-06-27	Claudio Sacerdoti...	Reloading bugged stylesheets no longer makes gTopLevel...	blob \| commitdiff \| raw \| diff to current
2003-06-27	Claudio Sacerdoti...	Reload stylesheets menu entry added (under the Settings...	blob \| commitdiff \| raw \| diff to current
2003-06-19	Claudio Sacerdoti...	* mquery_interpreter logging and debugging activated	blob \| commitdiff \| raw \| diff to current
2003-06-19	Claudio Sacerdoti...	Merge of the V7_3_new_exportation branch.	blob \| commitdiff \| raw \| diff to current
2002-10-21	natile	Merge of the new_mathql branch with the main branch:	blob \| commitdiff \| raw \| diff to current
2002-10-17	Enrico Tassi	- rewritesimpl_tac added in fourierR.ml (wrong location)	blob \| commitdiff \| raw \| diff to current
2002-10-14	Claudio Sacerdoti...	- bug fixed: some liftings were missing in the implemen...	blob \| commitdiff \| raw \| diff to current
2002-10-11	Claudio Sacerdoti...	New tactic rewrite implemented.	blob \| commitdiff \| raw \| diff to current
2002-09-27	Claudio Sacerdoti...	Better handling of queries. Now both the locate and...	blob \| commitdiff \| raw \| diff to current
2002-09-19	Enrico Tassi	Tactic update	blob \| commitdiff \| raw \| diff to current
2002-09-09	Claudio Sacerdoti...	When locate is used during the lexing phase, it may...	blob \| commitdiff \| raw \| diff to current
2002-09-04	Claudio Sacerdoti...	The parser (the lexer indeed) now use the locate query...	blob \| commitdiff \| raw \| diff to current
2002-09-04	Enrico Tassi	Fourier tactic	blob \| commitdiff \| raw \| diff to current
2002-08-29	Michele Galatà	Comment typo fixed.	blob \| commitdiff \| raw \| diff to current
2002-07-29	Claudio Sacerdoti...	Updated to use the new parser that creates (stacks...	blob \| commitdiff \| raw \| diff to current
2002-07-01	Stefano Zacchiroli	- added Ring tactic on reals	blob \| commitdiff \| raw \| diff to current
2002-07-01	Ferruccio Guidi	mathQL modified, stderr corrected to stdout im mathql_i...	blob \| commitdiff \| raw \| diff to current
2002-06-22	Ferruccio Guidi	untested version of mQueryGenerator (was mquery part 2)	blob \| commitdiff \| raw \| diff to current
2002-06-12	Claudio Sacerdoti...	* Abst removed from the DTD	blob \| commitdiff \| raw \| diff to current
2002-05-24	Claudio Sacerdoti...	* Clear and ClearBody implemented, but they are bugged...	blob \| commitdiff \| raw \| diff to current
2002-05-22	Claudio Sacerdoti...	Conjectures and Hypotheses inside every conjecture...	blob \| commitdiff \| raw \| diff to current
2002-05-21	Ferruccio Guidi	* empty log message *	blob \| commitdiff \| raw \| diff to current
2002-05-20	Claudio Sacerdoti...	mquery.ml now really call the execution of the query.	blob \| commitdiff \| raw \| diff to current
2002-05-20	Claudio Sacerdoti...	Many many improvements:	blob \| commitdiff \| raw \| diff to current
2002-05-08	Claudio Sacerdoti...	Experimental commit: definitions are now allowed in...	blob \| commitdiff \| raw \| diff to current
2002-04-30	Ferruccio Guidi	basic MathQL support	blob \| commitdiff \| raw \| diff to current
2002-04-29	Claudio Sacerdoti...	* Error handling improved	blob \| commitdiff \| raw \| diff to current
2002-04-26	Claudio Sacerdoti...	* Many improvements (expecially in exceptions handling)	blob \| commitdiff \| raw \| diff to current
2002-04-19	Claudio Sacerdoti...	* The interface of CicTypeChecker now allows the usage...	blob \| commitdiff \| raw \| diff to current
2002-04-19	Claudio Sacerdoti...	Reduction tactics in the scratch window implemented.	blob \| commitdiff \| raw \| diff to current
2002-04-18	Claudio Sacerdoti...	Scratch window is now also raised (= hide + show ;...	blob \| commitdiff \| raw \| diff to current
2002-04-18	Claudio Sacerdoti...	* Error reporting improved	blob \| commitdiff \| raw \| diff to current
2002-04-18	Claudio Sacerdoti...	* Scratch window added	blob \| commitdiff \| raw \| diff to current
2002-04-18	Claudio Sacerdoti...	* Many improvements	blob \| commitdiff \| raw \| diff to current
2002-04-16	Claudio Sacerdoti...	* Many improvements	blob \| commitdiff \| raw \| diff to current
2002-04-08	Claudio Sacerdoti...	* Many improvements	blob \| commitdiff \| raw \| diff to current
2002-04-05	Claudio Sacerdoti...	* Many improvements.	blob \| commitdiff \| raw \| diff to current
2002-04-02	Claudio Sacerdoti...	First commit of our future proof-assistant/proof-improv...	blob \| commitdiff \| raw \| diff to current

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom