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

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

2005-06-29	Claudio Sacerdoti...	Incredible bug of simpl fixed: the stack (in the terminology...	commit \| commitdiff \| tree
2005-06-29	Claudio Sacerdoti...	A few bug fixes. In particular parsing errors in matitatop...	commit \| commitdiff \| tree
2005-06-29	Claudio Sacerdoti...	does_not_occur unexported since it did not have the...	commit \| commitdiff \| tree
2005-06-29	Claudio Sacerdoti...	Removed a dummy "let ... in" that was there only to...	commit \| commitdiff \| tree
2005-06-29	Claudio Sacerdoti...	Stupid bug fixed in the refinement of let ... in	commit \| commitdiff \| tree
2005-06-29	Claudio Sacerdoti...	Informative message corrected: MatitacLib.go () is...	commit \| commitdiff \| tree
2005-06-28	Claudio Sacerdoti...	matitatop.ml is now a simple invocation of Toploop...	commit \| commitdiff \| tree
2005-06-28	Claudio Sacerdoti...	New solution: instead of using matitatop.bootstrap...	commit \| commitdiff \| tree
2005-06-28	Claudio Sacerdoti...	In case of EOI the "go ()" loop must exit!	commit \| commitdiff \| tree
2005-06-28	Claudio Sacerdoti...	matitatop	commit \| commitdiff \| tree
2005-06-28	Claudio Sacerdoti...	More complete bootstrapper.	commit \| commitdiff \| tree
2005-06-28	Claudio Sacerdoti...	New argument for LApply: the ident for the generated...	commit \| commitdiff \| tree
2005-06-28	Claudio Sacerdoti...	New argument for LApply: the ident for the generated...	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	New tactics.	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	replace generalized to patterns	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	1. interface of replace generalized to patterns	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	A few other tactics made available to matita.	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	A few other tactics made available to matita.	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	clear already exists	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	New argument (the identifier) to generalize.	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	New argument (the identifier) to generalize.	commit \| commitdiff \| tree
2005-06-27	Claudio Sacerdoti...	New argument (the hypothesis name) for cut.	commit \| commitdiff \| tree
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
next

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

RSS Atom