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-03-17	Claudio Sacerdoti...	...	tree \| commitdiff
2010-03-16	Claudio Sacerdoti...	Comparison of two applications with a different number...	tree \| commitdiff
2010-03-16	Claudio Sacerdoti...	1) intros cleans up the cache (because the context...	tree \| commitdiff
2010-03-16	Claudio Sacerdoti...	refreshing of inferred type was missing	tree \| commitdiff
2010-03-12	Andrea Asperti	Subst was missing in perforate small (apparently, gty...	tree \| commitdiff
2010-03-12	Andrea Asperti	removed debug from the inteface	tree \| commitdiff
2010-03-04	Andrea Asperti	In line with the ml.	tree \| commitdiff
2010-03-04	Andrea Asperti	1. For smart application, we only perforate small terms...	tree \| commitdiff
2010-03-04	Andrea Asperti	Small changes for debugging	tree \| commitdiff
2010-03-04	Andrea Asperti	Fixed a bug in deep_eq: we generated new clauses but...	tree \| commitdiff
2010-03-04	Andrea Asperti	Corrected a bug relative to the application of substs...	tree \| commitdiff
2010-03-02	Wilmer Ricciotti	Added syntax for ninversion tactic (still experimental).	tree \| commitdiff
2010-03-02	Enrico Tassi	Constants are indexed using the Reference, not the...	tree \| commitdiff
2010-03-01	Wilmer Ricciotti	Fixed a bug in the unification, which prevented some...	tree \| commitdiff
2010-02-19	Andrea Asperti	Open goals fixed (it also returned closed goals).	tree \| commitdiff
2010-02-19	Andrea Asperti	Removed debug printings.	tree \| commitdiff
2010-02-19	Andrea Asperti	added lazy	tree \| commitdiff
2010-02-19	Andrea Asperti	Nuova versione di auto.	tree \| commitdiff
2010-02-19	Andrea Asperti	Added an implicit parameter to branch_tac to allow...	tree \| commitdiff
2010-02-15	Claudio Sacerdoti...	The height of fixpoint applications was not computed...	tree \| commitdiff
2010-02-11	Enrico Tassi	minimal sequent height set to 1	tree \| commitdiff
2010-02-11	Enrico Tassi	some experiment filtering with height	tree \| commitdiff
2010-02-09	Andrea Asperti	Added a count_occurrences function.	tree \| commitdiff
2010-02-08	Andrea Asperti	Bug fixing.	tree \| commitdiff
2010-02-08	Andrea Asperti	Removed debug printings.	tree \| commitdiff
2010-02-08	Andrea Asperti	Some changes towards integration of setoid-rewriting.	tree \| commitdiff
2010-02-04	Andrea Asperti	Added count_occurrences.	tree \| commitdiff
2010-02-03	Claudio Sacerdoti...	...	tree \| commitdiff
2010-02-03	Wilmer Ricciotti	Disabled debug prints in ndestruct tactic.	tree \| commitdiff
2010-02-03	Claudio Sacerdoti...	Debug code commented out.	tree \| commitdiff
2010-02-03	Claudio Sacerdoti...	Parts of the status were not re-initialized correctly...	tree \| commitdiff
2010-02-03	Claudio Sacerdoti...	Bad variable name fixed.	tree \| commitdiff
2010-02-03	Claudio Sacerdoti...	Bug fixed: projection redexes obtained reducing other...	tree \| commitdiff
2010-02-02	Wilmer Ricciotti	New version using Streicher's K axiom. Should be faster...	tree \| commitdiff
2010-02-02	Wilmer Ricciotti	Fixed a bug with indexed inductive types which sometime...	tree \| commitdiff
2010-02-01	Andrea Asperti	On the last goal at maxdepth we stop at the first solution.	tree \| commitdiff
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
next

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

RSS Atom