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

]> matita.cs.unibo.it Git - helm.git/history - helm/software/components

[helm.git] / helm / software / components /

2010-01-29	Andrea Asperti	Nuova gestione della width.	tree \| commitdiff
2010-01-27	Andrea Asperti	Unfolded exact letins during proof reconstruction.	tree \| commitdiff
2010-01-27	Andrea Asperti	Added a parameter no_implicit (default true) to choose...	tree \| commitdiff
2010-01-18	Andrea Asperti	New paramod tac.	tree \| commitdiff
2010-01-18	Andrea Asperti	Invocation of paramod	tree \| commitdiff
2010-01-18	Andrea Asperti	paramod_tac exported	tree \| commitdiff
2010-01-18	Andrea Asperti	Number notation for NG	tree \| commitdiff
2010-01-18	Andrea Asperti	Number notation for NG	tree \| commitdiff
2010-01-18	Andrea Asperti	Number notation for NG.	tree \| commitdiff
2010-01-18	Andrea Asperti	Keeping Implicit for refinement (instead of transformin...	tree \| commitdiff
2010-01-12	Wilmer Ricciotti	Fixed a bug in the discrimination principle: the refine...	tree \| commitdiff
2010-01-11	Andrea Asperti	1. New paramodulation function	tree \| commitdiff
2010-01-11	Andrea Asperti	saturate cust be called with delta=0	tree \| commitdiff
2010-01-11	Andrea Asperti	Added is_equation	tree \| commitdiff
2010-01-11	Andrea Asperti	Debugging info	tree \| commitdiff
2010-01-08	Andrea Asperti	The body of constants is a reference, not the actual...	tree \| commitdiff
2010-01-08	Andrea Asperti	removed debugging info	tree \| commitdiff
2010-01-08	Andrea Asperti	applyS	tree \| commitdiff
2010-01-08	Andrea Asperti	refresh uri	tree \| commitdiff
2010-01-08	Andrea Asperti	Support for the new auto tactics //	tree \| commitdiff
2010-01-08	Andrea Asperti	Support for the new // tactics.	tree \| commitdiff
2010-01-08	Andrea Asperti	new reloc_subst (to avoid cyclic substitutions).	tree \| commitdiff
2009-12-21	Andrea Asperti	Refining with no expected type + unification seems...	tree \| commitdiff
2009-12-21	Andrea Asperti	Trying to be faster	tree \| commitdiff
2009-12-21	Andrea Asperti	Trying to be faster.	tree \| commitdiff
2009-12-18	Andrea Asperti	Final subst returned by superposition and passed around.	tree \| commitdiff
2009-12-18	Andrea Asperti	using = instead of alpha conversions. context metasenv...	tree \| commitdiff
2009-12-10	Andrea Asperti	Minor bag fixed, relative to failures.	tree \| commitdiff
2009-12-10	Andrea Asperti	A compiling version?	tree \| commitdiff
2009-12-09	Andrea Asperti	Added a "sort_metasenv" function.	tree \| commitdiff
2009-12-09	Andrea Asperti	Commented a couple of calls to "set_reference_of_oxuri".	tree \| commitdiff
2009-12-09	Andrea Asperti	Added the paramodulation stuff to the status	tree \| commitdiff
2009-12-09	Andrea Asperti	param "slir" to call the new auto	tree \| commitdiff
2009-12-09	Andrea Asperti	Added the paramodulation active/passive tables to the...	tree \| commitdiff
2009-12-09	Andrea Asperti	Attached fast_eq_check to auto	tree \| commitdiff
2009-12-09	Andrea Asperti	Added nnAuto.mli	tree \| commitdiff
2009-12-09	Andrea Asperti	Debug set to ()	tree \| commitdiff
2009-12-09	Andrea Asperti	Clean up of debgging info	tree \| commitdiff
2009-12-09	Andrea Asperti	Syntax error	tree \| commitdiff
2009-12-09	Andrea Asperti	Wrong reference corrected	tree \| commitdiff
2009-12-09	Andrea Asperti	Minor fixing for last chance	tree \| commitdiff
2009-12-09	Andrea Asperti	Added a fol operation	tree \| commitdiff
2009-12-04	Wilmer Ricciotti	Bugfix in inversion (was using refl_eq instead of refl).	tree \| commitdiff
2009-12-04	Andrea Asperti	Indexing local context for paramod.	tree \| commitdiff
2009-12-02	Andrea Asperti	The new paramodulation functions instantiated over...	tree \| commitdiff
2009-12-02	Andrea Asperti	New ways for initialising the signature required for...	tree \| commitdiff
2009-12-02	Andrea Asperti	Passive equations have their own index (not passive...	tree \| commitdiff
2009-12-02	Andrea Asperti	debug takes lazy strings. Moved here the are_alpha_eq...	tree \| commitdiff
2009-12-02	Andrea Asperti	Added a function remove_unit_clause	tree \| commitdiff
2009-12-02	Andrea Asperti	Added a boolean test function to discriminate equations...	tree \| commitdiff
2009-12-02	Andrea Asperti	Generalized intitialization for EqP	tree \| commitdiff
2009-12-02	Andrea Asperti	Generalized initialization of eqP.	tree \| commitdiff
2009-11-27	Wilmer Ricciotti	ndestruct now clears off identity equations whenever...	tree \| commitdiff
2009-11-25	Wilmer Ricciotti	Fixed inversion, which was broken by the last changes...	tree \| commitdiff
2009-11-25	Andrea Asperti	Exported forward_inference_step	tree \| commitdiff
2009-11-24	Wilmer Ricciotti	Bugfix in tipify: a metavariable was set to type withou...	tree \| commitdiff
2009-11-24	Wilmer Ricciotti	In order to prevent useless meta extensions, we optimiz...	tree \| commitdiff
2009-11-24	Wilmer Ricciotti	When unifying	tree \| commitdiff
2009-11-23	Andrea Asperti	Removed dead code	tree \| commitdiff
2009-11-23	Andrea Asperti	Subsumption and reduction	tree \| commitdiff
2009-11-19	Wilmer Ricciotti	- Added a swap parameter to the unification procedure	tree \| commitdiff
2009-11-18	Wilmer Ricciotti	NCicRefiner.force_to_sort implemented on top of NCicUni...	tree \| commitdiff
2009-11-18	Wilmer Ricciotti	Code factorization for check_type.	tree \| commitdiff
2009-11-17	Wilmer Ricciotti	ndestruct tactic: mainly bugfixes; the algorithm isn...	tree \| commitdiff
2009-11-17	Andrea Asperti	Closing the goal.	tree \| commitdiff
2009-11-16	Wilmer Ricciotti	Implementation of ndestruct tactic (including destructi...	tree \| commitdiff
2009-11-13	Andrea Asperti	Exported apply_subst_context	tree \| commitdiff
2009-11-13	Andrea Asperti	Added the new auto version (not attached yet).	tree \| commitdiff
2009-11-12	Claudio Sacerdoti...	Code made more uniform.	tree \| commitdiff
2009-11-10	Andrea Asperti	Union find slightly more general (f can now point to...	tree \| commitdiff
2009-11-05	Andrea Asperti	A case was missing	tree \| commitdiff
2009-11-05	Andrea Asperti	Naif version of the union find	tree \| commitdiff
2009-11-04	Claudio Sacerdoti...	Bug fixed: restrict used to take the list of positions...	tree \| commitdiff
2009-11-04	Claudio Sacerdoti...	1) sort computation undone (it used to be bugged anyway)	tree \| commitdiff
2009-10-30	Claudio Sacerdoti...	Code simplified.	tree \| commitdiff
2009-10-30	Claudio Sacerdoti...	Useless old code for ad-hoc management of out-scope...	tree \| commitdiff
2009-10-30	Claudio Sacerdoti...	New style debugging/profiling for NCicMetaSubst.	tree \| commitdiff
2009-10-30	Claudio Sacerdoti...	Sometimes it is useful to be able to print the subst...	tree \| commitdiff
2009-10-30	Enrico Tassi	auto snapshot	tree \| commitdiff
2009-10-29	Claudio Sacerdoti...	Better error message.	tree \| commitdiff
2009-10-29	Claudio Sacerdoti...	instantiate/sortfy/kindfy etc. reimplemented with less...	tree \| commitdiff
2009-10-29	Claudio Sacerdoti...	New function.	tree \| commitdiff
2009-10-29	Claudio Sacerdoti...	Let's use already existent functions.	tree \| commitdiff
2009-10-28	Claudio Sacerdoti...	Ad-hoc management of ? vs out_scope in instantiate...	tree \| commitdiff
2009-10-28	Claudio Sacerdoti...	Bug fixed: the `IsTerm attribute is now added by mk_met...	tree \| commitdiff
2009-10-28	Claudio Sacerdoti...	1) new-style debugging/profiling code for old reduction	tree \| commitdiff
2009-10-28	Claudio Sacerdoti...	Commented out code to optimize the case t1 vs t2 when...	tree \| commitdiff
2009-10-28	Claudio Sacerdoti...	One-shot aliases were no longer generated because of...	tree \| commitdiff
2009-10-28	Enrico Tassi	better indentation	tree \| commitdiff
2009-10-28	Enrico Tassi	better indentation	tree \| commitdiff
2009-10-28	Enrico Tassi	better comments and indentation	tree \| commitdiff
2009-10-28	Enrico Tassi	use prop_only to filter instead of repeting the same...	tree \| commitdiff
2009-10-28	Enrico Tassi	better logging	tree \| commitdiff
2009-10-28	Enrico Tassi	better logging and immediate pruning of new goals when	tree \| commitdiff
2009-10-28	Enrico Tassi	auto navigates a real tree, not a flattened one	tree \| commitdiff
2009-10-28	Enrico Tassi	labels in group_by_tac	tree \| commitdiff
2009-10-28	Enrico Tassi	new data structures for auto	tree \| commitdiff
2009-10-28	Enrico Tassi	do not put " around node name, otherwise names like...	tree \| commitdiff
2009-10-28	Enrico Tassi	export group_by_tac	tree \| commitdiff
2009-10-23	Enrico Tassi	added code to print the tree	tree \| commitdiff
next

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

RSS Atom