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

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

[helm.git] / helm / matita / matitaEngine.ml

2005-11-19	Claudio Sacerdoti...	Disambiguation errors are no longer thrown away. They...	blob \| commitdiff \| raw
2005-11-18	Enrico Tassi	fixed coercions undo	blob \| commitdiff \| raw \| diff to current
2005-11-03	Stefano Zacchiroli	better dependencies among modules and symlinking of...	blob \| commitdiff \| raw \| diff to current
2005-10-25	Stefano Zacchiroli	new tacticals	blob \| commitdiff \| raw \| diff to current
2005-10-25	Claudio Sacerdoti...	Every exception that used to have type string is now...	blob \| commitdiff \| raw \| diff to current
2005-10-17	Enrico Tassi	added coercions to Prod	blob \| commitdiff \| raw \| diff to current
2005-10-05	Stefano Zacchiroli	completed support for "-nodb", now also matitaclean...	blob \| commitdiff \| raw \| diff to current
2005-09-26	Alberto Griggio	new signature of auto_tac, with a new optional argument...	blob \| commitdiff \| raw \| diff to current
2005-09-26	Stefano Zacchiroli	- added integrity checks on .moo files	blob \| commitdiff \| raw \| diff to current
2005-09-23	Stefano Zacchiroli	changed .moo format on disk: no longer plain strings...	blob \| commitdiff \| raw \| diff to current
2005-09-23	Claudio Sacerdoti...	CicUtil.profile ==> HExtlib.profile	blob \| commitdiff \| raw \| diff to current
2005-09-23	Stefano Zacchiroli	bugfix: evaluation of object commands is now atomic...	blob \| commitdiff \| raw \| diff to current
2005-09-23	Enrico Tassi	universes are saved to disk	blob \| commitdiff \| raw \| diff to current
2005-09-23	Claudio Sacerdoti...	The disambiguation now returns the aliases diff. It...	blob \| commitdiff \| raw \| diff to current
2005-09-23	Claudio Sacerdoti...	The new_aliases argument of the functions alias_diff...	blob \| commitdiff \| raw \| diff to current
2005-09-21	Stefano Zacchiroli	ported to the new parser interface (Ulexing.lexbuf...	blob \| commitdiff \| raw \| diff to current
2005-09-19	Claudio Sacerdoti...	A bit of profiling functions added here and there.	blob \| commitdiff \| raw \| diff to current
2005-09-16	Enrico Tassi	added a function to reorder the metasenv.	blob \| commitdiff \| raw \| diff to current
2005-09-15	Claudio Sacerdoti...	Yet another implementation of the single aliases /...	blob \| commitdiff \| raw \| diff to current
2005-09-15	Stefano Zacchiroli	- changed command line interface of cicbrowser so that...	blob \| commitdiff \| raw \| diff to current
2005-09-13	Stefano Zacchiroli	- changed moo representation in MatitaTypes.status...	blob \| commitdiff \| raw \| diff to current
2005-09-12	Stefano Zacchiroli	Added support for multiple disambiguation passes.	blob \| commitdiff \| raw \| diff to current
2005-09-08	Stefano Zacchiroli	implemented lazy disambiguation of tactics arguments...	blob \| commitdiff \| raw \| diff to current
2005-09-05	Claudio Sacerdoti...	Assert false (for imbricated theorems) changed to a...	blob \| commitdiff \| raw \| diff to current
2005-09-02	Claudio Sacerdoti...	Unsharing removed since it is now used in Cic2acic.	blob \| commitdiff \| raw \| diff to current
2005-08-30	Claudio Sacerdoti...	A parser for aliases implemented (required by the Whelp).	blob \| commitdiff \| raw \| diff to current
2005-07-29	Claudio Sacerdoti...	0. core_notation.ma splitted into coq.moo and core_nota...	blob \| commitdiff \| raw \| diff to current
2005-07-28	Claudio Sacerdoti...	1. ProofEngineHelpers.locate_in_term, ProofEngineHelper...	blob \| commitdiff \| raw \| diff to current
2005-07-28	Claudio Sacerdoti...	New tactic unfold.	blob \| commitdiff \| raw \| diff to current
2005-07-27	Enrico Tassi	fixed matitamake to handle development with names with...	blob \| commitdiff \| raw \| diff to current
2005-07-22	Alberto Griggio	added optional "paramodulation" parameter to auto to...	blob \| commitdiff \| raw \| diff to current
2005-07-22	Claudio Sacerdoti...	Original semantics of a now almost random piece of...	blob \| commitdiff \| raw \| diff to current
2005-07-22	Claudio Sacerdoti...	Big changes:	blob \| commitdiff \| raw \| diff to current
2005-07-19	Stefano Zacchiroli	fixed file descriptor leak	blob \| commitdiff \| raw \| diff to current
2005-07-19	Enrico Tassi	message if the duplicate check may take too long	blob \| commitdiff \| raw \| diff to current
2005-07-19	Enrico Tassi	matitac now automatically cleans a non empty baseuri	blob \| commitdiff \| raw \| diff to current
2005-07-19	Ferruccio Guidi	the decompose tactic is now working	blob \| commitdiff \| raw \| diff to current
2005-07-18	Stefano Zacchiroli	added too .moo files notation related statements	blob \| commitdiff \| raw \| diff to current
2005-07-18	Stefano Zacchiroli	merged cic_notation with matita: good luck!	blob \| commitdiff \| raw \| diff to current
2005-07-15	Enrico Tassi	matitamake is integrated with matita	blob \| commitdiff \| raw \| diff to current
2005-07-15	Andrea Asperti	Bad name should be an error and not just a warning.	blob \| commitdiff \| raw \| diff to current
2005-07-13	Enrico Tassi	matitamake stuff:	blob \| commitdiff \| raw \| diff to current
2005-07-11	Enrico Tassi	added a flag to do the check of alredy-proved-theorem	blob \| commitdiff \| raw \| diff to current
2005-07-08	Enrico Tassi	added variant thm flavour	blob \| commitdiff \| raw \| diff to current
2005-07-08	Enrico Tassi	added query	blob \| commitdiff \| raw \| diff to current
2005-07-07	Claudio Sacerdoti...	1. Warnings are now printed in orange (yellow was unvis...	blob \| commitdiff \| raw \| diff to current
2005-07-07	Andrea Asperti	Raising an error on a bad theorem name.	blob \| commitdiff \| raw \| diff to current
2005-07-06	Enrico Tassi	check on baseuri	blob \| commitdiff \| raw \| diff to current
2005-07-06	Claudio Sacerdoti...	1. tactical "try_tacticals" renamed to "first"	blob \| commitdiff \| raw \| diff to current
2005-07-05	Ferruccio Guidi	name specifications added for elim_intros, elim_intros_...	blob \| commitdiff \| raw \| diff to current
2005-07-05	Enrico Tassi	now the moo contains also composed coercions (and It...	blob \| commitdiff \| raw \| diff to current
2005-07-05	Stefano Zacchiroli	ported to new getter interface	blob \| commitdiff \| raw \| diff to current
2005-07-04	Claudio Sacerdoti...	New command default "foo" uri1 ... urin	blob \| commitdiff \| raw \| diff to current
2005-07-04	Claudio Sacerdoti...	coercions are now stored in the .moo file.	blob \| commitdiff \| raw \| diff to current
2005-07-04	Claudio Sacerdoti...	Use eval_from_stream in place of eval_from_stream_ref...	blob \| commitdiff \| raw \| diff to current
2005-07-04	Claudio Sacerdoti...	"include" command implemented.	blob \| commitdiff \| raw \| diff to current
2005-07-04	Claudio Sacerdoti...	alias declarations are now put in the .moo file.	blob \| commitdiff \| raw \| diff to current
2005-07-01	Claudio Sacerdoti...	Signature of fwdSimpl changed to get rid of a warning.	blob \| commitdiff \| raw \| diff to current
2005-06-30	Claudio Sacerdoti...	Signature and concrete syntax of fold fixed.	blob \| commitdiff \| raw \| diff to current
2005-06-30	Ferruccio Guidi	lapply and fwd improved	blob \| commitdiff \| raw \| diff to current
2005-06-30	Claudio Sacerdoti...	1. rewrite_* and rewrite_back_* merged into one function	blob \| commitdiff \| raw \| diff to current
2005-06-30	Enrico Tassi	first matitadep snapshot	blob \| commitdiff \| raw \| diff to current
2005-06-29	Claudio Sacerdoti...	1. new syntax for patterns:	blob \| commitdiff \| raw \| diff to current
2005-06-29	Enrico Tassi	now baseuri is needed in each file (and its redefinitio...	blob \| commitdiff \| raw \| diff to current
2005-06-28	Enrico Tassi	* new binary matitatop	blob \| commitdiff \| raw \| diff to current
2005-06-28	Claudio Sacerdoti...	New argument for LApply: the ident for the generated...	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	replace generalized to patterns	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	A few other tactics made available to matita.	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	New argument (the identifier) to generalize.	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	New argument (the hypothesis name) for cut.	blob \| commitdiff \| raw \| diff to current
2005-06-27	Enrico Tassi	fized disambiguation of LApply	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	* the auto AST now has the width	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	* More tactics are now available to matita.	blob \| commitdiff \| raw \| diff to current
2005-06-25	Ferruccio Guidi	first working (?) version of lapply	blob \| commitdiff \| raw \| diff to current
2005-06-24	Ferruccio Guidi	lapply tactic continued	blob \| commitdiff \| raw \| diff to current
2005-06-24	Claudio Sacerdoti...	Asts generalized: a lot of tactics where restricted...	blob \| commitdiff \| raw \| diff to current
2005-06-23	Claudio Sacerdoti...	Tactic discriminate activated in matita.	blob \| commitdiff \| raw \| diff to current
2005-06-23	Claudio Sacerdoti...	1. Tactic generalize ported to patterns and activated...	blob \| commitdiff \| raw \| diff to current
2005-06-17	Enrico Tassi	support for goal patterns	blob \| commitdiff \| raw \| diff to current
2005-06-17	Claudio Sacerdoti...	more strings to UriManager.uri	blob \| commitdiff \| raw \| diff to current
2005-06-16	Stefano Zacchiroli	uses auto_tac_new instead of auto_tac	blob \| commitdiff \| raw \| diff to current
2005-06-16	Claudio Sacerdoti...	Dead code clean-up.	blob \| commitdiff \| raw \| diff to current
2005-06-15	Claudio Sacerdoti...	The `Record class now records also the name of the...	blob \| commitdiff \| raw \| diff to current
2005-06-15	Ferruccio Guidi	support for the new tactics lapply and fwd	blob \| commitdiff \| raw \| diff to current
2005-06-15	Claudio Sacerdoti...	Big commit and major code clean-up:	blob \| commitdiff \| raw \| diff to current
2005-06-13	Enrico Tassi	removed prerr_endline	blob \| commitdiff \| raw \| diff to current
2005-06-10	Enrico Tassi	added records	blob \| commitdiff \| raw \| diff to current
2005-06-10	Claudio Sacerdoti...	Got rid of a few bugs.	blob \| commitdiff \| raw \| diff to current
2005-06-09	Claudio Sacerdoti...	Error message improved.	blob \| commitdiff \| raw \| diff to current
2005-06-09	Enrico Tassi	added whd before uri_of_term	blob \| commitdiff \| raw \| diff to current
2005-06-08	Stefano Zacchiroli	rewritten cicBrowser handling of uri text entry, still...	blob \| commitdiff \| raw \| diff to current
2005-06-08	Claudio Sacerdoti...	More informative error message.	blob \| commitdiff \| raw \| diff to current
2005-06-07	Enrico Tassi	added letin	blob \| commitdiff \| raw \| diff to current
2005-06-01	Enrico Tassi	reduce with path	blob \| commitdiff \| raw \| diff to current
2005-06-01	Enrico Tassi	some cosmetic fixes	blob \| commitdiff \| raw \| diff to current
2005-05-31	Andrea Asperti	added automathic aliases for _ind _rec and _rect when...	blob \| commitdiff \| raw \| diff to current
2005-05-31	Enrico Tassi	added automathic aliases for qed and definition	blob \| commitdiff \| raw \| diff to current
2005-05-30	Andrea Asperti	added intros n.	blob \| commitdiff \| raw \| diff to current
2005-05-30	Andrea Asperti	added automathic aliases.	blob \| commitdiff \| raw \| diff to current
2005-05-27	Enrico Tassi	fixed matitac	blob \| commitdiff \| raw \| diff to current
next

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

RSS Atom