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

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

2005-07-04	Claudio Sacerdoti...	coercions are now stored in the .moo file.	commit \| commitdiff \| tree
2005-07-04	Claudio Sacerdoti...	Cosmetic changes.	commit \| commitdiff \| tree
2005-07-04	Claudio Sacerdoti...	New function (only partially implemented) to pretty...	commit \| commitdiff \| tree
2005-07-04	Claudio Sacerdoti...	Use eval_from_stream in place of eval_from_stream_ref...	commit \| commitdiff \| tree
2005-07-04	Claudio Sacerdoti...	include must not add aliases in the script!	commit \| commitdiff \| tree
2005-07-04	Claudio Sacerdoti...	"include" command implemented.	commit \| commitdiff \| tree
2005-07-04	Claudio Sacerdoti...	"include" command implemented.	commit \| commitdiff \| tree
2005-07-04	Claudio Sacerdoti...	alias declarations are now put in the .moo file.	commit \| commitdiff \| tree
2005-07-04	Claudio Sacerdoti...	Improvements in matitatop: instead of doing exit -1...	commit \| commitdiff \| tree
2005-07-03	Claudio Sacerdoti...	Equality tactics are now used in the first half of...	commit \| commitdiff \| tree
2005-07-02	Claudio Sacerdoti...	The equality tactics are now exploited.	commit \| commitdiff \| tree
2005-07-02	Claudio Sacerdoti...	All the equalityTactics have now been ported to use...	commit \| commitdiff \| tree
2005-07-02	Claudio Sacerdoti...	New theorem: eq_ind_r.	commit \| commitdiff \| tree
2005-07-02	Claudio Sacerdoti...	cosmetic change: a space removed (to make tests/Makefile...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	make tests and make tests.opt now call their counterparts...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	The tests are now in alphabetical order.	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	match.ma removed	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	* match.ma removed (it is now splitted in several files...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	conflicting baseuri	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	matitaclean is necessary!	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	* makefile improved	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	new targets:	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	New argument: the cleaner.	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	make all is now nicer	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	Two targets now:	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	make MATITAC="../scripts/do_tests.sh ../matitac /dev...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	Makefile improved	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	The library of matita is borned! Long life to the library...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	matitaclean.opt, matitadep.opt	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	TacticAst2Box no longer used.	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	Module TacticAst2Box unused!	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	count_pattern implemented	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	More cases implemented in tactic_count.	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	An interesting test for replace.	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	replace tactic reimplemented.	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	pattern_of function reimplemented. Now it takes a term...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	prerr_endline -> debug_print	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	Signature of fwdSimpl changed to get rid of a warning.	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	The replace tactic is now working again. It can now...	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	Signature of fwdSimpl changed to get rid of a warning.	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	matitaclean	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	New syntax for patterns.	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	1. change_tac moved from PrimitiveTactics to ReductionTactics	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	New test.	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	\vdash added	commit \| commitdiff \| tree
2005-07-01	Claudio Sacerdoti...	Syntax of patterns changed again to make it non-ambiguous:	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	Signature and concrete syntax of fold fixed.	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	The pattern of a fold cannot have the "wanted" part...	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	Signature and concrete syntax of fold fixed.	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	Text fixed (due to stricter semantics for naming the...	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	The rewrite_* set of tactics is now working again....	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	Bug fixed: a wrong lift made select unuseful when wanted...	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	Pretty printing of Cic.Implict (Some `Hole) is now "%"	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	1. rewrite_* and rewrite_back_* merged into one function	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	1. rewrite_* and rewrite_back_* merged into one function	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	Oooops. I forgot the convertibility test that makes...	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	baseuri put back	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	The tactic change is now working again. Moreover, it...	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	A bit of renaming in the code to make it more clear.	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	A simpler implementation of inversion that does not...	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	Obsolete comment removed.	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	Stupid bug fixed (a completely erroneous assert false...	commit \| commitdiff \| tree
2005-06-30	Claudio Sacerdoti...	This commit makes ProofEngineHelpers.select reach its...	commit \| commitdiff \| tree
2005-06-29	Claudio Sacerdoti...	1. new syntax for patterns:	commit \| commitdiff \| tree
2005-06-29	Claudio Sacerdoti...	1. new syntax for patterns:	commit \| commitdiff \| tree
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
next

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

RSS Atom