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

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

2007-05-29	Andrea Asperti	Corrected version od meta_convertibnility_subst.	commit \| commitdiff \| tree
2007-05-28	Andrea Asperti	Improved pruning (no propress).	commit \| commitdiff \| tree
2007-05-28	Andrea Asperti	Added a new version of meta_convertibnility that returns the	commit \| commitdiff \| tree
2007-05-09	Andrea Asperti	A few extensions for the moebius inversion theorem	commit \| commitdiff \| tree
2007-05-09	Andrea Asperti	Proof of the moebius inversion theorem	commit \| commitdiff \| tree
2007-04-30	Andrea Asperti	Even if we are at depth 0, we first check in the cache...	commit \| commitdiff \| tree
2007-04-30	Andrea Asperti	Removed an assert false; everything works again, but...	commit \| commitdiff \| tree
2007-04-27	Andrea Asperti	Subst is passed in input to apapluy, so no need to...	commit \| commitdiff \| tree
2007-04-27	Andrea Asperti	Apply_with_subst now returns a subst with a correct...	commit \| commitdiff \| tree
2007-04-24	Andrea Asperti	Subsumption_subst re-added to initial.	commit \| commitdiff \| tree
2007-04-24	Andrea Asperti	@	commit \| commitdiff \| tree
2007-03-16	Andrea Asperti	New contrib moebius.ma.	commit \| commitdiff \| tree
2007-03-16	Andrea Asperti	Extensions required for the moebius function (in Z).	commit \| commitdiff \| tree
2007-03-13	Andrea Asperti	Few theorems added.`	commit \| commitdiff \| tree
2007-03-13	Andrea Asperti	new version of div_and_mod	commit \| commitdiff \| tree
2007-03-13	Andrea Asperti	Capturing Invalid_argument inside pp (otherwise we...	commit \| commitdiff \| tree
2007-01-16	Andrea Asperti	Added SetoidInc.m	commit \| commitdiff \| tree
2007-01-16	Andrea Asperti	Some CoRN files.	commit \| commitdiff \| tree
2006-12-22	Andrea Asperti	Add_moo_content modified to avoid repetitions of index...	commit \| commitdiff \| tree
2006-12-22	Andrea Asperti	Minor change.	commit \| commitdiff \| tree
2006-12-22	Andrea Asperti	Collapse_head_metas transforms all terms "not-recongnized...	commit \| commitdiff \| tree
2006-12-22	Andrea Asperti	In the let-in case we compute the type and add it to...	commit \| commitdiff \| tree
2006-12-22	Andrea Asperti	The function uri_of_term now works also if the explciit...	commit \| commitdiff \| tree
2006-12-18	Andrea Asperti	M logic/coimplication.ma	commit \| commitdiff \| tree
2006-12-18	Andrea Asperti	Renamed iterative into map_iter_p and moved around...	commit \| commitdiff \| tree
2006-12-18	Andrea Asperti	Proof of Euler theorem.	commit \| commitdiff \| tree
2006-11-29	Andrea Asperti	Demodulate_tac now depends on the universe	commit \| commitdiff \| tree
2006-11-28	Andrea Asperti	Changed an ahstable into an association list.	commit \| commitdiff \| tree
2006-11-27	Andrea Asperti	Added in_eq_uris.	commit \| commitdiff \| tree
2006-11-27	Andrea Asperti	Fix_proof should recursively work on explicit substs.	commit \| commitdiff \| tree
2006-11-27	Andrea Asperti	Removed a couple of assertions.	commit \| commitdiff \| tree
2006-11-27	Andrea Asperti	Commented an assertion.	commit \| commitdiff \| tree
2006-11-27	Andrea Asperti	Commented an assertion.	commit \| commitdiff \| tree
2006-11-27	Andrea Asperti	Commented a few assertions.	commit \| commitdiff \| tree
2006-11-27	Andrea Asperti	Variant are not indexed.	commit \| commitdiff \| tree
2006-11-27	Andrea Asperti	Only modified for taking unfold into account.	commit \| commitdiff \| tree
2006-11-27	Andrea Asperti	Matita's default equality has changed	commit \| commitdiff \| tree
2006-11-27	Andrea Asperti	Small changes	commit \| commitdiff \| tree
2006-11-23	Andrea Asperti	Command index added to disambiguate.	commit \| commitdiff \| tree
2006-11-23	Andrea Asperti	Added a new command "index" for the indexing terms...	commit \| commitdiff \| tree
2006-11-23	Andrea Asperti	Set of Set of uri added.	commit \| commitdiff \| tree
2006-11-23	Andrea Asperti	Modifications to auto due to the introduction of the...	commit \| commitdiff \| tree
2006-11-23	Andrea Asperti	Universe is a discrimination-tree structure.	commit \| commitdiff \| tree
2006-11-23	Andrea Asperti	The status has been extended with a "universe", that...	commit \| commitdiff \| tree
2006-11-23	Andrea Asperti	Fixed a call to auto, and commented the remaining part.	commit \| commitdiff \| tree
2006-11-23	Andrea Asperti	paramodulation removed	commit \| commitdiff \| tree
2006-11-23	Andrea Asperti	Minor changes.	commit \| commitdiff \| tree
2006-11-23	Andrea Asperti	Simplified version.	commit \| commitdiff \| tree
2006-11-23	Andrea Asperti	Adding CoRN.	commit \| commitdiff \| tree
2006-11-15	Andrea Asperti	lt_O_S moved to nat/orders.ma	commit \| commitdiff \| tree
2006-11-15	Andrea Asperti	Added lt_O_S.	commit \| commitdiff \| tree
2006-10-30	Andrea Asperti	library = yes!	commit \| commitdiff \| tree
2006-10-25	Andrea Asperti	Added a couple of flags to auto	commit \| commitdiff \| tree
2006-10-20	Andrea Asperti	Demodulate and applyS moved form saturation to auto.	commit \| commitdiff \| tree
2006-10-20	Andrea Asperti	Major changes to auto, documented on the helm mailing...	commit \| commitdiff \| tree
2006-10-20	Andrea Asperti	Minor changes.	commit \| commitdiff \| tree
2006-10-20	Andrea Asperti	a. uniform mangement for context and library	commit \| commitdiff \| tree
2006-10-20	Andrea Asperti	The type of universe_of_goals has slightly changed...	commit \| commitdiff \| tree
2006-10-20	Andrea Asperti	This is only a temporary patch. The typecheker raises a	commit \| commitdiff \| tree
2006-10-20	Andrea Asperti	The function exists_a_meta has been modified to capture...	commit \| commitdiff \| tree
2006-10-20	Andrea Asperti	New function pack_coercion_metasenv, used in auto after...	commit \| commitdiff \| tree
2006-10-09	Andrea Asperti	Theorems from the library and from the context are...	commit \| commitdiff \| tree
2006-10-09	Andrea Asperti	The two coercions sym_eq e eq_f gives BIG TROUBLES...	commit \| commitdiff \| tree
2006-10-09	Andrea Asperti	Factorized "find_equalities" in demodulation_tac.	commit \| commitdiff \| tree
2006-10-03	Andrea Asperti	Changed auto from implicit to option and renamed a...	commit \| commitdiff \| tree
2006-09-04	Andrea Asperti	Generation of inductive and inversion principles for...	commit \| commitdiff \| tree
2006-09-04	Andrea Asperti	Bug fixing. If the inductive types do not occur in...	commit \| commitdiff \| tree
2006-07-24	Andrea Asperti	Bug fixed: a symbol alias Symb(s,0) now subsumes the...	commit \| commitdiff \| tree
2006-07-24	Andrea Asperti	A compiling version of the library.	commit \| commitdiff \| tree
2006-07-14	Andrea Asperti	Added the computation of max_weight.	commit \| commitdiff \| tree
2006-07-14	Andrea Asperti	Added the computation of max_weight for equations in...	commit \| commitdiff \| tree
2006-06-29	Andrea Asperti	Cleaning up; removed a couple of "open".	commit \| commitdiff \| tree
2006-06-19	Andrea Asperti	some experiments	commit \| commitdiff \| tree
2006-06-19	Andrea Asperti	added (but still unused) remove_local_context	commit \| commitdiff \| tree
2006-06-19	Andrea Asperti	added (but not yet used) remove_local_context	commit \| commitdiff \| tree
2006-06-19	Andrea Asperti	Utils.compare_terms instead of compare_weights	commit \| commitdiff \| tree
2006-06-19	Andrea Asperti	occur_check and unification fixed. now Meta(i,[]) and...	commit \| commitdiff \| tree
2006-06-15	Andrea Asperti	some examples of the new ApplyS tactic	commit \| commitdiff \| tree
2006-06-15	Andrea Asperti	examples of applyS	commit \| commitdiff \| tree
2006-06-15	Andrea Asperti	Apply-Silvie tactic added!	commit \| commitdiff \| tree
2006-06-15	Andrea Asperti	added applyS	commit \| commitdiff \| tree
2006-06-15	Andrea Asperti	some fixed done in Orsay:	commit \| commitdiff \| tree
2006-06-15	Andrea Asperti	exported 2 functions needed by applyS	commit \| commitdiff \| tree
2006-06-15	Andrea Asperti	...	commit \| commitdiff \| tree
2006-06-15	Andrea Asperti	default constants are now the matita standard library...	commit \| commitdiff \| tree
2006-06-09	Andrea Asperti	Notation for congruent.	commit \| commitdiff \| tree
2006-06-01	Andrea Asperti	Subsumption_subst must be applied to the initial proof...	commit \| commitdiff \| tree
2006-05-26	Andrea Asperti	1) variables occurring only in proofs anre not relocated	commit \| commitdiff \| tree
2006-05-26	Andrea Asperti	Bug fixed: the syntax "?n" used to be broken. It tried...	commit \| commitdiff \| tree
2006-05-23	Andrea Asperti	added important comment	commit \| commitdiff \| tree
2006-05-23	Andrea Asperti	fixed LetIn proofs	commit \| commitdiff \| tree
2006-05-23	Andrea Asperti	added stuff for profiling macros	commit \| commitdiff \| tree
2006-05-05	Andrea Asperti	New version of deep_subsumption	commit \| commitdiff \| tree
2006-04-27	Andrea Asperti	Equality chains.	commit \| commitdiff \| tree
2006-04-27	Andrea Asperti	Added is_trans_eq_URI and is_sym_eq_URI	commit \| commitdiff \| tree
2006-04-26	Andrea Asperti	Build_proof_goal does not return the metasenv any more.	commit \| commitdiff \| tree
2006-04-26	Andrea Asperti	fixed demodulation_goal (used to return always false)	commit \| commitdiff \| tree
2006-04-26	Andrea Asperti	removed ocaml equality on equations	commit \| commitdiff \| tree
2006-04-10	Andrea Asperti	Removed negative equations.	commit \| commitdiff \| tree
2006-04-04	Andrea Asperti	Naif substitution. Removed local context in metas during...	commit \| commitdiff \| tree
next

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

RSS Atom