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

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

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
2006-03-27	Andrea Asperti	args removed from equalities.	commit \| commitdiff \| tree
2006-03-24	Andrea Asperti	New unification and new matching.	commit \| commitdiff \| tree
2006-03-23	Andrea Asperti	Best parameter setting for de morgan.	commit \| commitdiff \| tree
2006-03-22	Andrea Asperti	:	commit \| commitdiff \| tree
2006-03-21	Andrea Asperti	Changed the type of compute-equality_weight that now...	commit \| commitdiff \| tree
2006-03-20	Andrea Asperti	Renamed SK.ma into bool.ma	commit \| commitdiff \| tree
2006-03-20	Andrea Asperti	Esempi di auto.	commit \| commitdiff \| tree
2006-03-20	Andrea Asperti	Snapshot.	commit \| commitdiff \| tree
2006-02-06	Andrea Asperti	termine bacato.	commit \| commitdiff \| tree
2006-02-06	Andrea Asperti	fixed usage of matita.auto_disambiguation	commit \| commitdiff \| tree
2006-02-06	Andrea Asperti	Bug?	commit \| commitdiff \| tree

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

RSS Atom