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

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

2009-12-09	Andrea Asperti	Added a "sort_metasenv" function.	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Commented a couple of calls to "set_reference_of_oxuri".	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Added the paramodulation stuff to the status	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	param "slir" to call the new auto	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Added the paramodulation active/passive tables to the...	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Attached fast_eq_check to auto	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Added nnAuto.mli	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Debug set to ()	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Clean up of debgging info	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Syntax error	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Wrong reference corrected	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Minor fixing for last chance	commit \| commitdiff \| tree \| snapshot
2009-12-09	Andrea Asperti	Added a fol operation	commit \| commitdiff \| tree \| snapshot
2009-12-04	Wilmer Ricciotti	Bugfix in inversion (was using refl_eq instead of refl).	commit \| commitdiff \| tree \| snapshot
2009-12-04	Andrea Asperti	Indexing local context for paramod.	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Propositional equality	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	The new paramodulation functions instantiated over...	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	New ways for initialising the signature required for...	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Passive equations have their own index (not passive...	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	debug takes lazy strings. Moved here the are_alpha_eq...	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Added a function remove_unit_clause	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Added a boolean test function to discriminate equations...	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Generalized intitialization for EqP	commit \| commitdiff \| tree \| snapshot
2009-12-02	Andrea Asperti	Generalized initialization of eqP.	commit \| commitdiff \| tree \| snapshot
2009-12-01	Enrico Tassi	porting to lablgtk2 >= 2.14 and releasing	commit \| commitdiff \| tree \| snapshot
2009-12-01	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-11-27	Wilmer Ricciotti	ndestruct now clears off identity equations whenever...	commit \| commitdiff \| tree \| snapshot
2009-11-25	Wilmer Ricciotti	Fixed inversion, which was broken by the last changes...	commit \| commitdiff \| tree \| snapshot
2009-11-25	Andrea Asperti	Exported forward_inference_step	commit \| commitdiff \| tree \| snapshot
2009-11-24	Wilmer Ricciotti	Bugfix in tipify: a metavariable was set to type withou...	commit \| commitdiff \| tree \| snapshot
2009-11-24	Wilmer Ricciotti	In order to prevent useless meta extensions, we optimiz...	commit \| commitdiff \| tree \| snapshot
2009-11-24	Wilmer Ricciotti	When unifying	commit \| commitdiff \| tree \| snapshot
2009-11-23	Andrea Asperti	Removed dead code	commit \| commitdiff \| tree \| snapshot
2009-11-23	Andrea Asperti	Subsumption and reduction	commit \| commitdiff \| tree \| snapshot
2009-11-19	Wilmer Ricciotti	- Added a swap parameter to the unification procedure	commit \| commitdiff \| tree \| snapshot
2009-11-18	Wilmer Ricciotti	NCicRefiner.force_to_sort implemented on top of NCicUni...	commit \| commitdiff \| tree \| snapshot
2009-11-18	Wilmer Ricciotti	Code factorization for check_type.	commit \| commitdiff \| tree \| snapshot
2009-11-17	Wilmer Ricciotti	ndestruct tactic: mainly bugfixes; the algorithm isn...	commit \| commitdiff \| tree \| snapshot
2009-11-17	Andrea Asperti	Closing the goal.	commit \| commitdiff \| tree \| snapshot
2009-11-16	Wilmer Ricciotti	Implementation of ndestruct tactic (including destructi...	commit \| commitdiff \| tree \| snapshot
2009-11-13	Andrea Asperti	Exported apply_subst_context	commit \| commitdiff \| tree \| snapshot
2009-11-13	Andrea Asperti	Added the new auto version (not attached yet).	commit \| commitdiff \| tree \| snapshot
2009-11-12	Ferruccio Guidi	some interfaces improved	commit \| commitdiff \| tree \| snapshot
2009-11-12	Claudio Sacerdoti...	Code made more uniform.	commit \| commitdiff \| tree \| snapshot
2009-11-10	Andrea Asperti	Union find slightly more general (f can now point to...	commit \| commitdiff \| tree \| snapshot
2009-11-05	Andrea Asperti	A case was missing	commit \| commitdiff \| tree \| snapshot
2009-11-05	Ferruccio Guidi	brg: change in the representation of binders	commit \| commitdiff \| tree \| snapshot
2009-11-05	Andrea Asperti	Naif version of the union find	commit \| commitdiff \| tree \| snapshot
2009-11-04	Claudio Sacerdoti...	Bug fixed: restrict used to take the list of positions...	commit \| commitdiff \| tree \| snapshot
2009-11-04	Claudio Sacerdoti...	1) sort computation undone (it used to be bugged anyway)	commit \| commitdiff \| tree \| snapshot
2009-11-03	Ferruccio Guidi	basic_rg: reduction was not tail recursive by mistake	commit \| commitdiff \| tree \| snapshot
2009-10-30	Claudio Sacerdoti...	Code simplified.	commit \| commitdiff \| tree \| snapshot
2009-10-30	Claudio Sacerdoti...	Useless old code for ad-hoc management of out-scope...	commit \| commitdiff \| tree \| snapshot
2009-10-30	Claudio Sacerdoti...	New style debugging/profiling for NCicMetaSubst.	commit \| commitdiff \| tree \| snapshot
2009-10-30	Claudio Sacerdoti...	Sometimes it is useful to be able to print the subst...	commit \| commitdiff \| tree \| snapshot
2009-10-30	Enrico Tassi	auto snapshot	commit \| commitdiff \| tree \| snapshot
2009-10-29	Ferruccio Guidi	- dual_rg: renamed to complete_rg [as suggested in...	commit \| commitdiff \| tree \| snapshot
2009-10-29	Ferruccio Guidi	refactoring ...	commit \| commitdiff \| tree \| snapshot
2009-10-29	Ferruccio Guidi	new xml exportation procedure for basic_rg (10 times...	commit \| commitdiff \| tree \| snapshot
2009-10-29	Claudio Sacerdoti...	Better error message.	commit \| commitdiff \| tree \| snapshot
2009-10-29	Claudio Sacerdoti...	For some obscure reason, more universes are now needed...	commit \| commitdiff \| tree \| snapshot
2009-10-29	Claudio Sacerdoti...	instantiate/sortfy/kindfy etc. reimplemented with less...	commit \| commitdiff \| tree \| snapshot
2009-10-29	Claudio Sacerdoti...	New function.	commit \| commitdiff \| tree \| snapshot
2009-10-29	Claudio Sacerdoti...	Let's use already existent functions.	commit \| commitdiff \| tree \| snapshot
2009-10-28	Ferruccio Guidi	- lambda-delta: some fixes: now the grundlagen type...	commit \| commitdiff \| tree \| snapshot
2009-10-28	Claudio Sacerdoti...	Works again	commit \| commitdiff \| tree \| snapshot
2009-10-28	Claudio Sacerdoti...	Ad-hoc management of ? vs out_scope in instantiate...	commit \| commitdiff \| tree \| snapshot
2009-10-28	Claudio Sacerdoti...	Bug fixed: the `IsTerm attribute is now added by mk_met...	commit \| commitdiff \| tree \| snapshot
2009-10-28	Claudio Sacerdoti...	1) new-style debugging/profiling code for old reduction	commit \| commitdiff \| tree \| snapshot
2009-10-28	Claudio Sacerdoti...	Commented out code to optimize the case t1 vs t2 when...	commit \| commitdiff \| tree \| snapshot
2009-10-28	Claudio Sacerdoti...	One-shot aliases were no longer generated because of...	commit \| commitdiff \| tree \| snapshot
2009-10-28	Claudio Sacerdoti...	Different aliases, better equality inferred.	commit \| commitdiff \| tree \| snapshot
2009-10-28	Claudio Sacerdoti...	instances	commit \| commitdiff \| tree \| snapshot
2009-10-28	Claudio Sacerdoti...	instance fixed	commit \| commitdiff \| tree \| snapshot
2009-10-28	Enrico Tassi	better indentation	commit \| commitdiff \| tree \| snapshot
2009-10-28	Enrico Tassi	better indentation	commit \| commitdiff \| tree \| snapshot
2009-10-28	Enrico Tassi	better comments and indentation	commit \| commitdiff \| tree \| snapshot
2009-10-28	Enrico Tassi	use prop_only to filter instead of repeting the same...	commit \| commitdiff \| tree \| snapshot
2009-10-28	Enrico Tassi	better logging	commit \| commitdiff \| tree \| snapshot
2009-10-28	Enrico Tassi	better logging and immediate pruning of new goals when	commit \| commitdiff \| tree \| snapshot
2009-10-28	Enrico Tassi	auto navigates a real tree, not a flattened one	commit \| commitdiff \| tree \| snapshot
2009-10-28	Enrico Tassi	labels in group_by_tac	commit \| commitdiff \| tree \| snapshot
2009-10-28	Enrico Tassi	new data structures for auto	commit \| commitdiff \| tree \| snapshot
2009-10-28	Enrico Tassi	do not put " around node name, otherwise names like...	commit \| commitdiff \| tree \| snapshot
2009-10-28	Enrico Tassi	export group_by_tac	commit \| commitdiff \| tree \| snapshot
2009-10-28	Ferruccio Guidi	drg->brg translation contibued (still bugged though)	commit \| commitdiff \| tree \| snapshot
2009-10-26	Claudio Sacerdoti...	qed => nqed.	commit \| commitdiff \| tree \| snapshot
2009-10-26	Claudio Sacerdoti...	Now the time required to eval a command is printed.	commit \| commitdiff \| tree \| snapshot
2009-10-23	Enrico Tassi	added code to print the tree	commit \| commitdiff \| tree \| snapshot
2009-10-23	Enrico Tassi	CSC proof made by paramod	commit \| commitdiff \| tree \| snapshot
2009-10-23	Enrico Tassi	more functions	commit \| commitdiff \| tree \| snapshot
2009-10-23	Claudio Sacerdoti...	Alias required now ??	commit \| commitdiff \| tree \| snapshot
2009-10-22	Enrico Tassi	new instantiate, only known bug is w.r.t. in/out scope...	commit \| commitdiff \| tree \| snapshot
2009-10-22	Enrico Tassi	the trie indexes terms up to 10 nested applications...	commit \| commitdiff \| tree \| snapshot
2009-10-22	Enrico Tassi	more auto	commit \| commitdiff \| tree \| snapshot
2009-10-21	Claudio Sacerdoti...	Non general recursion implemented via recursion over...	commit \| commitdiff \| tree \| snapshot
2009-10-21	Enrico Tassi	first bits for the zipper	commit \| commitdiff \| tree \| snapshot
2009-10-21	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-10-21	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-10-21	Enrico Tassi	more printings	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom