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

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

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

2005-01-19	Enrico Tassi	coercion application	blob \| commitdiff \| raw
2005-01-17	Enrico Tassi	new cicEnvironment implementation	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	- pass subst to FreshNameGenerator on mk_fresh_name...	blob \| commitdiff \| raw \| diff to current
2004-11-25	Stefano Zacchiroli	protected invocations of get_cooked_obj with assertion...	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-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-01	Enrico Tassi	new universes implementation	blob \| commitdiff \| raw \| diff to current
2004-04-23	Enrico Tassi	Universes introduction	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-05	Claudio Sacerdoti...	Refine now raises only RefineFailure, AssertFailure...	blob \| commitdiff \| raw \| diff to current
2004-03-02	Claudio Sacerdoti...	- Improved error messaging.	blob \| commitdiff \| raw \| diff to current
2004-02-26	Claudio Sacerdoti...	Error message fixed.	blob \| commitdiff \| raw \| diff to current
2004-02-26	Claudio Sacerdoti...	New implementation of eat_prods.	blob \| commitdiff \| raw \| diff to current
2004-02-26	Claudio Sacerdoti...	Optimization: since an invariant says that the inferred...	blob \| commitdiff \| raw \| diff to current
2004-02-11	Claudio Sacerdoti...	Big changes:	blob \| commitdiff \| raw \| diff to current
2004-02-09	Claudio Sacerdoti...	eat_prods now uses mk_implicit_type.	blob \| commitdiff \| raw \| diff to current
2004-02-07	Claudio Sacerdoti...	- Added mk_implicit_sort.	blob \| commitdiff \| raw \| diff to current
2004-02-07	Claudio Sacerdoti...	sort_of_prod: the second term, when it is a meta, was...	blob \| commitdiff \| raw \| diff to current
2004-02-06	Stefano Zacchiroli	added annotations to Cic.Implicit	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	Improved error messages.	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	- sort_of_prod now returns the second Meta (if it is...	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	No longer puts anonymous declarations in the canonical...	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	- the result of a refinement is now cleared from dummy...	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	dummy dependent types and dummy letins are now removed...	blob \| commitdiff \| raw \| diff to current
2004-02-04	Stefano Zacchiroli	- improved some error messages	blob \| commitdiff \| raw \| diff to current
2004-02-03	Claudio Sacerdoti...	sort_of_prod changed to not generate a new metavariable...	blob \| commitdiff \| raw \| diff to current
2004-02-03	Claudio Sacerdoti...	eat_prods reimplemented to generalize the output type...	blob \| commitdiff \| raw \| diff to current
2004-02-02	Stefano Zacchiroli	- refine's type_of no longer return a substitution	blob \| commitdiff \| raw \| diff to current
2004-02-02	Stefano Zacchiroli	- removed metasenv argument from kernel proxies invocations	blob \| commitdiff \| raw \| diff to current
2004-01-29	Claudio Sacerdoti...	- lift added to CicMetaSubst	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-23	Stefano Zacchiroli	a better error message	blob \| commitdiff \| raw \| diff to current
2004-01-22	Stefano Zacchiroli	bugfixes, typos and the hell	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-02	Ferruccio Guidi	sort CProp added	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

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

RSS Atom