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

]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/cic_proof_checking/cicTypeChecker.ml

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

2004-04-23	Enrico Tassi	Universes introduction	blob \| commitdiff \| raw
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...	Wrong error message patched.	blob \| commitdiff \| raw \| diff to current
2004-03-02	Claudio Sacerdoti...	Bug in guarded_by_destructors (case Rel to a definition...	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-24	Claudio Sacerdoti...	Partial porting to V8 URIs.	blob \| commitdiff \| raw \| diff to current
2004-02-10	Claudio Sacerdoti...	Bug fixed: checking inductive type declarations with...	blob \| commitdiff \| raw \| diff to current
2004-02-09	Claudio Sacerdoti...	sort_of_prod now thinks that a "sort metavariable"...	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...	sort_of_prod relaxed to accept also Metas (when the...	blob \| commitdiff \| raw \| diff to current
2004-02-03	Stefano Zacchiroli	removed SortExpectedMetaFound special exception	blob \| commitdiff \| raw \| diff to current
2004-02-02	Stefano Zacchiroli	- added SortExpectedMetaFound exception (huge hack)	blob \| commitdiff \| raw \| diff to current
2004-01-27	Stefano Zacchiroli	use CicUtil.lookup_meta	blob \| commitdiff \| raw \| diff to current
2004-01-22	Stefano Zacchiroli	better exception and error messages	blob \| commitdiff \| raw \| diff to current
2003-12-16	Stefano Zacchiroli	renamed module "logger" to "cicLogger" to avoid confusi...	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
2002-06-19	Claudio Sacerdoti...	* empty log message *	blob \| commitdiff \| raw \| diff to current
2002-06-12	Claudio Sacerdoti...	Abst removed from the DTD.	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-26	Claudio Sacerdoti...	Bug fixed in type_of_aux (Cast case).	blob \| commitdiff \| raw \| diff to current
2002-04-19	Claudio Sacerdoti...	* env renamed to context everywhere in cicTypeChecker.ml	blob \| commitdiff \| raw \| diff to current
2002-04-16	Claudio Sacerdoti...	Module Logger added.	blob \| commitdiff \| raw \| diff to current
2002-04-16	Andrea Asperti	Meta implemented.	blob \| commitdiff \| raw \| diff to current
2001-12-12	Claudio Sacerdoti...	Fixing of guarded_by_constructors completed.	blob \| commitdiff \| raw \| diff to current
2001-12-11	Claudio Sacerdoti...	PARTIAL COMMIT:	blob \| commitdiff \| raw \| diff to current
2001-12-10	Claudio Sacerdoti...	Bug fixed: the strictly_positive condition was unnecess...	blob \| commitdiff \| raw \| diff to current
2001-12-07	Claudio Sacerdoti...	The typing rule for LetIn was simply wrong. Fixed.	blob \| commitdiff \| raw \| diff to current
2001-12-07	Claudio Sacerdoti...	Bug partially fixed: the branch of a case of type Prod...	blob \| commitdiff \| raw \| diff to current
2001-12-05	Claudio Sacerdoti...	Very stupid bug fixed: in is_small, I created an enviro...	blob \| commitdiff \| raw \| diff to current
2001-12-05	Claudio Sacerdoti...	The definition of small inductive types has been relaxe...	blob \| commitdiff \| raw \| diff to current
2001-12-05	Claudio Sacerdoti...	Just code clean-up.	blob \| commitdiff \| raw \| diff to current
2001-12-04	Claudio Sacerdoti...	* Code improvement: there were two different functions...	blob \| commitdiff \| raw \| diff to current
2001-12-04	Claudio Sacerdoti...	does_not_occur now handles LetIn correctly (i.e. raisin...	blob \| commitdiff \| raw \| diff to current
2001-12-04	Claudio Sacerdoti...	Error reporting improved.	blob \| commitdiff \| raw \| diff to current
2001-12-04	Claudio Sacerdoti...	is_small did not use the environment. Hence the List...	blob \| commitdiff \| raw \| diff to current
2001-12-04	Claudio Sacerdoti...	decast must also perform LetIn reduction now.	blob \| commitdiff \| raw \| diff to current
2001-12-03	Claudio Sacerdoti...	* Major code cleanup.	blob \| commitdiff \| raw \| diff to current
2001-11-30	Claudio Sacerdoti...	Exception management improved.	blob \| commitdiff \| raw \| diff to current
2001-11-26	Claudio Sacerdoti...	HELM OCaml libraries with findlib support.	blob \| commitdiff \| raw \| diff to current

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

RSS Atom