matita.cs.unibo.it Git - helm.git/search

]> matita.cs.unibo.it Git - helm.git/search

2005-06-27	Claudio Sacerdoti...	New syntax of auto: auto [depth = n] [width = m].	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	* the auto AST now has the width	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	More tactics or tactic arguments made available to...	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	* auto_tac removed (it can be found in CVS)	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	* More tactics are now available to matita.	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	More tactics are now available to matita.	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	Nicer output for the "make tests*" commands.	commit \| commitdiff \| tree
2005-06-24	Claudio Sacerdoti...	New implementation of experimental_hint/auto (called...	commit \| commitdiff \| tree
2005-06-24	Claudio Sacerdoti...	Bug fixed: select => select distinct (since the ors...	commit \| commitdiff \| tree
2005-06-24	Claudio Sacerdoti...	cicPxpParser.ml, cicParser2.ml and cicParser3.ml...	commit \| commitdiff \| tree
2005-06-24	Claudio Sacerdoti...	Small improvement in extracting suffixes.	commit \| commitdiff \| tree
2005-06-24	Claudio Sacerdoti...	New functions UriManager.uri_is_var, UriManager.uri_is_con.	commit \| commitdiff \| tree
2005-06-24	Claudio Sacerdoti...	Asts generalized: a lot of tactics where restricted...	commit \| commitdiff \| tree
2005-06-24	Claudio Sacerdoti...	debugging printf removed	commit \| commitdiff \| tree
2005-06-23	Claudio Sacerdoti...	Tactic discriminate activated in matita.	commit \| commitdiff \| tree
2005-06-23	Claudio Sacerdoti...	The discriminate tactic accepts a term, not only an...	commit \| commitdiff \| tree
2005-06-23	Claudio Sacerdoti...	1. Tactic generalize ported to patterns and activated...	commit \| commitdiff \| tree
2005-06-23	Claudio Sacerdoti...	Tactic generalize ported to patterns and activated...	commit \| commitdiff \| tree
2005-06-23	Claudio Sacerdoti...	1 .Tactic generalize ported to patterns and activated...	commit \| commitdiff \| tree
2005-06-17	Claudio Sacerdoti...	more strings to UriManager.uri	commit \| commitdiff \| tree
2005-06-17	Claudio Sacerdoti...	many strings that are supposed to be URIs are now UriManager.uri	commit \| commitdiff \| tree
2005-06-16	Claudio Sacerdoti...	Locally implemented print_context replaced by CicPp...	commit \| commitdiff \| tree
2005-06-16	Claudio Sacerdoti...	Dead code clean-up.	commit \| commitdiff \| tree
2005-06-16	Claudio Sacerdoti...	Dead code for packing/unpacking (usually just a big...	commit \| commitdiff \| tree
2005-06-16	Claudio Sacerdoti...	Dead code clean-up.	commit \| commitdiff \| tree
2005-06-16	Claudio Sacerdoti...	matita.conf.xml added	commit \| commitdiff \| tree
2005-06-16	Claudio Sacerdoti...	removed again (I added it by error :-(	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	* parsing errors in tests were not detected and the...	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	Syntax of <attributes>...</attributes> improved to...	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	DTD for attributes revised.	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	The `Record class now records also the name of the...	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	a parser error is now logged as an error!	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	Bug fixed: parsing errors were ignored by matitac since...	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	Bug fixed (that used to throw away a metasenv :-(	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	Refinement of CurrentProof did not check whether the...	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	Big commit and major code clean-up:	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	comments syntax changed	commit \| commitdiff \| tree
2005-06-15	Claudio Sacerdoti...	incomplete proof completed.	commit \| commitdiff \| tree
2005-06-14	Claudio Sacerdoti...	* no more %% comments	commit \| commitdiff \| tree
2005-06-14	Claudio Sacerdoti...	No more %% comments.	commit \| commitdiff \| tree
2005-06-14	Claudio Sacerdoti...	parentheses allowed inside comments	commit \| commitdiff \| tree
2005-06-14	Claudio Sacerdoti...	test_lexer and test_parser compiled by default	commit \| commitdiff \| tree
2005-06-14	Claudio Sacerdoti...	incomplete proof completed	commit \| commitdiff \| tree
2005-06-14	Claudio Sacerdoti...	typo fixed: simmetry ==> symmetry	commit \| commitdiff \| tree
2005-06-14	Claudio Sacerdoti...	incomplete proof terminated	commit \| commitdiff \| tree
2005-06-14	Claudio Sacerdoti...	qed missing	commit \| commitdiff \| tree
2005-06-14	Claudio Sacerdoti...	Bug fixed: when the final proof_status is not No_proof...	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	The type of the left parameters of an inductive type...	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	Got rid of a few bugs.	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	Got rid of a few warnings.	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	Got rid of a few warnings.	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	an assert failure changed to an exception and a bit...	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	The user is no longer obliged to give the types for...	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	debugging to false	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	* (Head) beta reduction functions factorized	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	More debugging infos.	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	unshare.ml*	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	Complete unsharing of terms.	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	head_beta_reduce used to create applications of applications...	commit \| commitdiff \| tree
2005-06-10	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-06-09	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-06-09	Claudio Sacerdoti...	test_instance.ma moved to interactive/ (whose tests...	commit \| commitdiff \| tree
2005-06-09	Claudio Sacerdoti...	intro ==> intros	commit \| commitdiff \| tree
2005-06-09	Claudio Sacerdoti...	Error message improved.	commit \| commitdiff \| tree
2005-06-09	Claudio Sacerdoti...	Now CicMetaSubst.delift_rels restricts the Metas when...	commit \| commitdiff \| tree
2005-06-09	Claudio Sacerdoti...	No more explicit types for the branches of the matches...	commit \| commitdiff \| tree
2005-06-09	Claudio Sacerdoti...	CicSubstitution.delift ==> CicMetaSubst.delift_rels	commit \| commitdiff \| tree
2005-06-09	Claudio Sacerdoti...	Exception raised by delift changed:	commit \| commitdiff \| tree
2005-06-09	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree
2005-06-09	Claudio Sacerdoti...	andrea.ma removed (superseded by match.ma)	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	The type of a top-level "let rec" can be optional.	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	Let's try to make the "let rec" construct infer its...	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	Syntax for top-level "let rec" fixed.	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	Using the lighter syntax for "let recs".	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	Using the top-level syntax for let-rec definitions.	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	The file is now well formed.	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	New syntax (again) for let rec binders:	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	New lighter syntax for "let rec".	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	Bug fixed: a symbol must be formed of just one (unicode...	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	Query results were erroneously tagged as directories.	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	1. syntax of match changed	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	Yet another bug fixed in the inference of the outtype...	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	The getter maps are now dumped also if matitac exits...	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	Added new target "make tests" for regression testing.	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	Fixed a few bugs in the inference of the outtype for...	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	Fixed inference of outtype for match when the inductive...	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	Harder test (with empty inductive types and left and...	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	More informative error message.	commit \| commitdiff \| tree
2005-06-08	Claudio Sacerdoti...	clean now also performs clean_metas (since make also...	commit \| commitdiff \| tree
2005-05-26	Claudio Sacerdoti...	Now the links to 7 pages at a time are shown. Cool.	commit \| commitdiff \| tree
2005-05-26	Claudio Sacerdoti...	256 chars max ==> 1024 chars max (because of Coq)	commit \| commitdiff \| tree
2005-05-26	Claudio Sacerdoti...	Bugs fixed:	commit \| commitdiff \| tree
2005-05-23	Claudio Sacerdoti...	Added sql/drop_mowgli_tables.mysql.sql	commit \| commitdiff \| tree
2005-03-22	Claudio Sacerdoti...	Bug fixed in assumption_tac: a missing (lift n) when...	commit \| commitdiff \| tree
2004-11-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2004-10-14	Claudio Sacerdoti...	Luca (bugged) debugging stuff removed.	commit \| commitdiff \| tree
2004-10-14	Claudio Sacerdoti...	no_inconcl_aux managed	commit \| commitdiff \| tree
next

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

RSS Atom