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

2007-01-02	Enrico Tassi	added oblivion_universe and used it in paxck_coercions	blob \| commitdiff \| raw
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