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

]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/cic_unification/cicUnification.ml

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

2005-11-19	Claudio Sacerdoti...	Less verbose error messages (= substitution applied...	blob \| commitdiff \| raw
2005-11-18	Enrico Tassi	more work for coercions	blob \| commitdiff \| raw \| diff to current
2005-11-14	Enrico Tassi	dded missing catch for coercions	blob \| commitdiff \| raw \| diff to current
2005-11-07	Claudio Sacerdoti...	AssertFailure from the type-checker now becomes an...	blob \| commitdiff \| raw \| diff to current
2005-10-25	Stefano Zacchiroli	"better" (????) identification of assertion failures	blob \| commitdiff \| raw \| diff to current
2005-10-25	Claudio Sacerdoti...	Every exception that used to have type string is now...	blob \| commitdiff \| raw \| diff to current
2005-09-26	Claudio Sacerdoti...	Unification enhanchement:	blob \| commitdiff \| raw \| diff to current
2005-09-21	Claudio Sacerdoti...	More debug_print made lazy.	blob \| commitdiff \| raw \| diff to current
2005-09-19	Claudio Sacerdoti...	This commit (partially) removes a big source of ineffic...	blob \| commitdiff \| raw \| diff to current
2005-09-15	Stefano Zacchiroli	uniformed ppmetasenv to other pp* methods: substs are...	blob \| commitdiff \| raw \| diff to current
2005-09-09	Enrico Tassi	the case Appl Meta vs t was not executed in case t...	blob \| commitdiff \| raw \| diff to current
2005-06-10	Claudio Sacerdoti...	* (Head) beta reduction functions factorized	blob \| commitdiff \| raw \| diff to current
2005-05-31	Enrico Tassi	implemented normalize (used in new_metasenv_for_apply)	blob \| commitdiff \| raw \| diff to current
2005-05-27	Enrico Tassi	removed debug prerr_endline	blob \| commitdiff \| raw \| diff to current
2005-05-27	Andrea Asperti	1. removed obsolete comments	blob \| commitdiff \| raw \| diff to current
2005-05-20	Andrea Asperti	When we unify a Prod against a term t2 which is not...	blob \| commitdiff \| raw \| diff to current
2005-04-27	Stefano Zacchiroli	merged changes from the svn fork by me and Enrico	blob \| commitdiff \| raw \| diff to current
2005-02-14	Enrico Tassi	Added heuristic in the Appl case, we beta-expand only...	blob \| commitdiff \| raw \| diff to current
2004-12-01	Enrico Tassi	Added universes handling. The PRE_UNIVERSES tag may...	blob \| commitdiff \| raw \| diff to current
2004-11-29	Stefano Zacchiroli	passes subst to FreshNameGenerator	blob \| commitdiff \| raw \| diff to current
2004-10-22	Andrea Asperti	- ported to typed explicit subst	blob \| commitdiff \| raw \| diff to current
2004-07-20	Andrea Asperti	Subst has been added to the kernel.	blob \| commitdiff \| raw \| diff to current
2004-07-05	Stefano Zacchiroli	Bug fixed: beta_expand did not perform any recursion...	blob \| commitdiff \| raw \| diff to current
2004-07-02	Claudio Sacerdoti...	Bug fixed: the beta_expansion function did not lift...	blob \| commitdiff \| raw \| diff to current
2004-07-01	Stefano Zacchiroli	New handling of substitution:	blob \| commitdiff \| raw \| diff to current
2004-06-28	Andrea Asperti	- new implementation of the apply case in fo_unif using...	blob \| commitdiff \| raw \| diff to current
2004-06-18	Claudio Sacerdoti...	- In the case (?i args) vs term the term is now eta...	blob \| commitdiff \| raw \| diff to current
2004-04-23	Enrico Tassi	Universes introduction	blob \| commitdiff \| raw \| diff to current
2004-04-22	Enrico Tassi	Big bug fixed: in the case t <?= ?1, the instantiation...	blob \| commitdiff \| raw \| diff to current
2004-03-16	Andrea Asperti	Sorts are no longer all convertible. To be completed...	blob \| commitdiff \| raw \| diff to current
2004-03-02	Claudio Sacerdoti...	...	blob \| commitdiff \| raw \| diff to current
2004-03-02	Claudio Sacerdoti...	- Improved error messaging.	blob \| commitdiff \| raw \| diff to current
2004-02-11	Stefano Zacchiroli	fixed typo	blob \| commitdiff \| raw \| diff to current
2004-02-11	Claudio Sacerdoti...	A type checking error report now prints also the metasenv.	blob \| commitdiff \| raw \| diff to current
2004-02-11	Claudio Sacerdoti...	Big changes:	blob \| commitdiff \| raw \| diff to current
2004-02-06	Stefano Zacchiroli	added annotations to Cic.Implicit	blob \| commitdiff \| raw \| diff to current
2004-02-03	Stefano Zacchiroli	catch just AssertFailure instead of _ (AssertFailure...	blob \| commitdiff \| raw \| diff to current
2004-02-03	Claudio Sacerdoti...	Meta vs same Meta now tries unification when convertibi...	blob \| commitdiff \| raw \| diff to current
2004-02-02	Stefano Zacchiroli	uses CicMetaSubst.ppterm where needed	blob \| commitdiff \| raw \| diff to current
2004-02-02	Stefano Zacchiroli	- big hack: keep on unifying/refining when SortExpected...	blob \| commitdiff \| raw \| diff to current
2004-01-27	Stefano Zacchiroli	- occur check test anticipated to the delift phase	blob \| commitdiff \| raw \| diff to current
2004-01-22	Stefano Zacchiroli	added to CicMetaSubst subst wrapper for CicReduction...	blob \| commitdiff \| raw \| diff to current
2004-01-22	Stefano Zacchiroli	- splitted into cicMetaSubst	blob \| commitdiff \| raw \| diff to current
2004-01-20	Andrea Asperti	First version of refine for MutCase, still largely...	blob \| commitdiff \| raw \| diff to current
2003-12-18	Claudio Sacerdoti...	Bug commented out. The comment is also commented.	blob \| commitdiff \| raw \| diff to current
2003-12-18	Claudio Sacerdoti...	Big bug spotted: restriction can fail and it was implic...	blob \| commitdiff \| raw \| diff to current
2003-12-18	Claudio Sacerdoti...	One of the bug I detected (and commented) in my last...	blob \| commitdiff \| raw \| diff to current
2003-12-17	Claudio Sacerdoti...	More comments. Some of them may highlight bugs or open...	blob \| commitdiff \| raw \| diff to current
2003-12-17	Claudio Sacerdoti...	Big bug spotted and commented: the delift function...	blob \| commitdiff \| raw \| diff to current
2003-12-17	Claudio Sacerdoti...	* comments improved an possible code weakness (i.e...	blob \| commitdiff \| raw \| diff to current
2003-12-17	Claudio Sacerdoti...	* Reindentation.	blob \| commitdiff \| raw \| diff to current
2003-09-05	Claudio Sacerdoti...	Defs in context may now have an optional type (when...	blob \| commitdiff \| raw \| diff to current
2003-06-19	Claudio Sacerdoti...	Merge of the V7_3_new_exportation branch.	blob \| commitdiff \| raw \| diff to current
2002-06-12	Claudio Sacerdoti...	Abst removed from the DTD.	blob \| commitdiff \| raw \| diff to current
2002-05-22	Claudio Sacerdoti...	delift moved from cicSubstitution to cicUnification	blob \| commitdiff \| raw \| diff to current
2002-05-20	Claudio Sacerdoti...	New experimental commit: metavariables representation...	blob \| commitdiff \| raw \| diff to current
2002-05-08	Claudio Sacerdoti...	Experimental commit: we can now have definitions in...	blob \| commitdiff \| raw \| diff to current
2002-04-29	Claudio Sacerdoti...	Bug fixed: the unwinding was not recursively performed...	blob \| commitdiff \| raw \| diff to current
2002-04-26	Claudio Sacerdoti...	Old and dead code from the previous implementation...	blob \| commitdiff \| raw \| diff to current
2002-04-26	Claudio Sacerdoti...	First (very bugged) version of cic_unification committed.	blob \| commitdiff \| raw \| diff to current

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

RSS Atom