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

2004-04-23	Enrico Tassi	Universes introduction	blob \| commitdiff \| raw
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