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

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

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

2009-06-09	Claudio Sacerdoti...	Debugging code removed.	blob \| commitdiff \| raw
2009-06-09	Claudio Sacerdoti...	Temporary (and partially broken) patch for Ferruccio...	blob \| commitdiff \| raw \| diff to current
2009-05-15	Claudio Sacerdoti...	Patch to add a debugging string to HExtlib.split_nth...	blob \| commitdiff \| raw
2009-05-14	Ferruccio Guidi	- hExtlib: added debugging information for split_nth	blob \| commitdiff \| raw \| diff to current
2009-04-28	Enrico Tassi	huge commit in automation:	blob \| commitdiff \| raw
2009-01-26	Enrico Tassi	added a number to identical error messages to ease...	blob \| commitdiff \| raw \| diff to current
2009-01-15	Enrico Tassi	unvariant also for coercions to funclass	blob \| commitdiff \| raw \| diff to current
2009-01-15	Enrico Tassi	coercions that are marked as variant are unfolded when...	blob \| commitdiff \| raw \| diff to current
2009-01-13	Enrico Tassi	many changes regarding coercions:	blob \| commitdiff \| raw \| diff to current
2008-12-24	Enrico Tassi	bug fixed, all convertible was called without a metasenv	blob \| commitdiff \| raw \| diff to current
2008-12-19	Enrico Tassi	identity coercions are not really inserted, just used...	blob \| commitdiff \| raw \| diff to current
2008-12-18	Claudio Sacerdoti...	Stupid bug fixed: checkin the type in place of the...	blob \| commitdiff \| raw \| diff to current
2008-12-18	Claudio Sacerdoti...	Now it compiles again.	blob \| commitdiff \| raw \| diff to current
2008-12-18	Claudio Sacerdoti...	Refinement of axioms fixed. We did not check that the...	blob \| commitdiff \| raw \| diff to current
2008-12-15	Enrico Tassi	To check if a term is type, do a whd of its sort before...	blob \| commitdiff \| raw \| diff to current
2008-11-28	Ferruccio Guidi	ng_disambiguation ng_kernel ng_refiner disambiguation...	blob \| commitdiff \| raw \| diff to current
2008-11-15	Enrico Tassi	missing subst added, now apply rule is probably enough...	blob \| commitdiff \| raw \| diff to current
2008-11-15	Enrico Tassi	disambiguation can use a goal as hint for the expected...	blob \| commitdiff \| raw \| diff to current
2008-09-18	Claudio Sacerdoti...	In case of coercion to Prod, the error message shown...	blob \| commitdiff \| raw \| diff to current
2008-07-15	Enrico Tassi	CProp_i <= Type_i , Type_i <= CProp_i	blob \| commitdiff \| raw \| diff to current
2008-07-10	Enrico Tassi	fixed regression in casting an argument to funclass...	blob \| commitdiff \| raw \| diff to current
2008-07-09	Enrico Tassi	CProp hierarchy fixed:	blob \| commitdiff \| raw \| diff to current
2008-07-07	Enrico Tassi	simplified coercDb implementation with additional info...	blob \| commitdiff \| raw \| diff to current
2008-06-13	Enrico Tassi	replace assert false with AssertFailure	blob \| commitdiff \| raw \| diff to current
2008-06-11	Enrico Tassi	meta not considered before in outtype	blob \| commitdiff \| raw \| diff to current
2008-05-30	Enrico Tassi	CProp hierarchy is there!	blob \| commitdiff \| raw \| diff to current
2008-05-29	Enrico Tassi	the type of the match was obtained reducing the outtype	blob \| commitdiff \| raw \| diff to current
2008-05-18	Enrico Tassi	using the right names in the context to check match...	blob \| commitdiff \| raw \| diff to current
2008-05-18	Claudio Sacerdoti...	This commit avoids cleaning dummy dependent types in...	blob \| commitdiff \| raw \| diff to current
2008-04-22	Enrico Tassi	oblivion ugraph everywhere outside the kernel	blob \| commitdiff \| raw \| diff to current
2008-04-17	Enrico Tassi	new calculation of recursive parameters in guarded...	blob \| commitdiff \| raw \| diff to current
2008-03-11	Claudio Sacerdoti...	Very experimental commit: the type of the source is...	blob \| commitdiff \| raw \| diff to current
2008-03-10	Claudio Sacerdoti...	check_metasenv_consistency:	blob \| commitdiff \| raw \| diff to current
2007-12-04	Claudio Sacerdoti...	Even if the error is not localized, it was not a good...	blob \| commitdiff \| raw \| diff to current
2007-12-04	Claudio Sacerdoti...	Some terms are not localized from the very beginning :-(	blob \| commitdiff \| raw \| diff to current
2007-12-04	Claudio Sacerdoti...	One more error localized. But the code is really ugly...	blob \| commitdiff \| raw \| diff to current
2007-11-28	Claudio Sacerdoti...	Bug fixed: an unification exception used to escape...	blob \| commitdiff \| raw \| diff to current
2007-11-25	Claudio Sacerdoti...	Bug fixed: an unification exception used to escape...	blob \| commitdiff \| raw \| diff to current
2007-11-23	Enrico Tassi	restored the right context used to generate names....	blob \| commitdiff \| raw \| diff to current
2007-11-15	Enrico Tassi	removed ugly prerr_endline	blob \| commitdiff \| raw \| diff to current
2007-11-15	Enrico Tassi	added ~delta parameter to saturate_term and used it...	blob \| commitdiff \| raw \| diff to current
2007-10-26	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2007-10-25	Claudio Sacerdoti...	Bug fixed: a MutCase considering a wrong number of...	blob \| commitdiff \| raw \| diff to current
2007-10-25	Claudio Sacerdoti...	Recently introduced bug fixed: error localization was...	blob \| commitdiff \| raw \| diff to current
2007-09-19	Enrico Tassi	commented out pack coercion, since the code is not...	blob \| commitdiff \| raw \| diff to current
2007-09-09	Enrico Tassi	in the case of coerce_to_sort the whd was done with...	blob \| commitdiff \| raw \| diff to current
2007-09-08	Enrico Tassi	huge commit regarding coercions to funclass and eat_pro...	blob \| commitdiff \| raw \| diff to current
2007-09-07	Enrico Tassi	1. fix_arity fixed: the code is totally wrong and this...	blob \| commitdiff \| raw \| diff to current
2007-09-07	Enrico Tassi	when a coercion is passed through a case on right-param...	blob \| commitdiff \| raw \| diff to current
2007-09-07	Enrico Tassi	ooops, missing )	blob \| commitdiff \| raw \| diff to current
2007-09-07	Enrico Tassi	fixed propagation under Fix/Lambda/Case of coercions...	blob \| commitdiff \| raw \| diff to current
2007-09-06	Enrico Tassi	coercions under Fix and Case. Code refactoring needed	blob \| commitdiff \| raw \| diff to current
2007-09-05	Claudio Sacerdoti...	coercions are propagated under Fix (but not mutually...	blob \| commitdiff \| raw \| diff to current
2007-08-31	Enrico Tassi	fixed coercions between arrows when the arrow is dependent.	blob \| commitdiff \| raw \| diff to current
2007-08-30	Enrico Tassi	captured exception preserved (was replaced blindly...	blob \| commitdiff \| raw \| diff to current
2007-08-30	Enrico Tassi	refactoring of all coercions code and add a check to...	blob \| commitdiff \| raw \| diff to current
2007-08-30	Enrico Tassi	Coercions rework:	blob \| commitdiff \| raw \| diff to current
2007-07-19	Enrico Tassi	COERCIONS: tentative addition of an equivalence relatio...	blob \| commitdiff \| raw \| diff to current
2007-06-23	Enrico Tassi	removed ugly printings	blob \| commitdiff \| raw \| diff to current
2007-04-12	Enrico Tassi	HACK for indtype checking	blob \| commitdiff \| raw \| diff to current
2007-04-05	Enrico Tassi	many printings added	blob \| commitdiff \| raw \| diff to current
2007-02-02	Claudio Sacerdoti...	Serious bug fixed: the types of a real mutual fix defin...	blob \| commitdiff \| raw \| diff to current
2007-01-30	Claudio Sacerdoti...	Behaviour of CicRefine.type_of_aux' on MutCases changed...	blob \| commitdiff \| raw \| diff to current
2007-01-02	Enrico Tassi	added oblivion_universe and used it in paxck_coercions	blob \| commitdiff \| raw \| diff to current
2006-12-28	Claudio Sacerdoti...	Yet another localization error in eat_prods fixed.	blob \| commitdiff \| raw \| diff to current
2006-12-14	Claudio Sacerdoti...	Huge commit:	blob \| commitdiff \| raw \| diff to current
2006-11-25	Enrico Tassi	added assertion (that is a TODO) in case non-considered...	blob \| commitdiff \| raw \| diff to current
2006-11-12	Claudio Sacerdoti...	The pretty printers in CicPp now have an optional ...	blob \| commitdiff \| raw \| diff to current
2006-10-28	Claudio Sacerdoti...	GRAVE BUG IN COERCIONS FIXED: the insertion of a coerci...	blob \| commitdiff \| raw \| diff to current
2006-10-25	Claudio Sacerdoti...	1. is_meta_closed should be applied only to terms on...	blob \| commitdiff \| raw \| diff to current
2006-10-23	Claudio Sacerdoti...	Better (and more localized) error message for sort_of_prod.	blob \| commitdiff \| raw \| diff to current
2006-10-23	Claudio Sacerdoti...	CicUniv.UniverseInconsistency is no handled correcly.	blob \| commitdiff \| raw \| diff to current
2006-10-20	Andrea Asperti	New function pack_coercion_metasenv, used in auto after...	blob \| commitdiff \| raw \| diff to current
2006-10-19	Claudio Sacerdoti...	Bug fixed: when trying to insert coercions after an...	blob \| commitdiff \| raw \| diff to current
2006-10-18	Claudio Sacerdoti...	Too verbose error message (probably activated by Enrico...	blob \| commitdiff \| raw \| diff to current
2006-10-09	Claudio Sacerdoti...	Bugs fixed in merging of composite coercions. In partic...	blob \| commitdiff \| raw \| diff to current
2006-10-06	Claudio Sacerdoti...	1. some "try ... with _ " removed	blob \| commitdiff \| raw \| diff to current
2006-09-15	Claudio Sacerdoti...	Yet another refinement error localized.	blob \| commitdiff \| raw \| diff to current
2006-09-15	Claudio Sacerdoti...	Debugging code deactivated.	blob \| commitdiff \| raw \| diff to current
2006-09-05	Enrico Tassi	fixed coercions. composite can't occur if to funclass	blob \| commitdiff \| raw \| diff to current
2006-09-04	Enrico Tassi	BIG FAT COMMIT REGARDING COERCIONS:	blob \| commitdiff \| raw \| diff to current
2006-07-10	Enrico Tassi	improved coercions support:	blob \| commitdiff \| raw \| diff to current
2006-05-26	Claudio Sacerdoti...	Recently introduced bug in CicRefine.eat_prods fixed...	blob \| commitdiff \| raw \| diff to current
2006-05-26	Claudio Sacerdoti...	Great optimization for eat_prods: if the type of the...	blob \| commitdiff \| raw \| diff to current
2006-04-26	Enrico Tassi	added a whd (nodelta) in the carr function used by...	blob \| commitdiff \| raw \| diff to current
2006-04-13	Claudio Sacerdoti...	Ugly solution to the "we proved T that is equivalent...	blob \| commitdiff \| raw \| diff to current
2006-02-20	Claudio Sacerdoti...	pack_coercion used to avoid packing n-ary coercions...	blob \| commitdiff \| raw \| diff to current
2006-02-20	Claudio Sacerdoti...	Localization bug fixed.	blob \| commitdiff \| raw \| diff to current
2006-02-20	Claudio Sacerdoti...	Bug fixed in pack_coercions_obj. The context of the...	blob \| commitdiff \| raw \| diff to current
2006-02-18	Claudio Sacerdoti...	Bug fixed in insertion of parametric coercions.	blob \| commitdiff \| raw \| diff to current
2006-02-18	Claudio Sacerdoti...	More refinement errors localized.	blob \| commitdiff \| raw \| diff to current
2006-02-18	Claudio Sacerdoti...	More refinement errors localized.	blob \| commitdiff \| raw \| diff to current
2006-02-18	Claudio Sacerdoti...	Bug fixed: the wrong exception was enriched, breaking...	blob \| commitdiff \| raw \| diff to current
2006-02-15	Enrico Tassi	added support for "polymorphic" coercions	blob \| commitdiff \| raw \| diff to current
2006-02-03	Stefano Zacchiroli	- renamed ocaml/ to components/	blob \| commitdiff \| raw \| diff to current

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

RSS Atom