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

2005-11-03	Claudio Sacerdoti...	Semantic change: I always consider a type with no const...	blob \| commitdiff \| raw
2005-11-03	Claudio Sacerdoti...	Semantic change: elimination of a term whose type is...	blob \| commitdiff \| raw \| diff to current
2005-11-03	Claudio Sacerdoti...	1. a simplified version of check_allowed_sort_eliminati...	blob \| commitdiff \| raw \| diff to current
2005-11-03	Claudio Sacerdoti...	Major code semplification in check_allowed_sort_elimina...	blob \| commitdiff \| raw \| diff to current
2005-10-25	Enrico Tassi	moved the expansion of implicits inside the refiner...	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-10-25	Claudio Sacerdoti...	~subst fixed everywhere in the type-checker:	blob \| commitdiff \| raw \| diff to current
2005-10-25	Claudio Sacerdoti...	Bug fixed: the current substitution and metasenv were...	blob \| commitdiff \| raw \| diff to current
2005-10-03	Enrico Tassi	the filled object is inserted in the env after a succes...	blob \| commitdiff \| raw \| diff to current
2005-09-23	Claudio Sacerdoti...	Profiling code removed.	blob \| commitdiff \| raw \| diff to current
2005-09-23	Enrico Tassi	added universes list handling	blob \| commitdiff \| raw \| diff to current
2005-09-21	Enrico Tassi	clean_and_fill optimization	blob \| commitdiff \| raw \| diff to current
2005-09-21	Claudio Sacerdoti...	More debug_print made lazy.	blob \| commitdiff \| raw \| diff to current
2005-09-05	Claudio Sacerdoti...	Bug fixed: Invalid_argument was raised by List.combine...	blob \| commitdiff \| raw \| diff to current
2005-09-02	Claudio Sacerdoti...	Serious bug fixed previously introduced by me in the...	blob \| commitdiff \| raw \| diff to current
2005-07-11	Claudio Sacerdoti...	Bug fixed in check_sort_elimination in the case (not...	blob \| commitdiff \| raw \| diff to current
2005-06-15	Claudio Sacerdoti...	Big commit and major code clean-up:	blob \| commitdiff \| raw \| diff to current
2005-06-10	Claudio Sacerdoti...	* (Head) beta reduction functions factorized	blob \| commitdiff \| raw \| diff to current
2005-06-07	Enrico Tassi	added whd to match argument in guarded_by_destructors;	blob \| commitdiff \| raw \| diff to current
2005-05-31	Andrea Asperti	more verbose case failure message	blob \| commitdiff \| raw \| diff to current
2005-05-27	Enrico Tassi	removed debug prerr_endline	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-01-21	Stefano Zacchiroli	attributes support	blob \| commitdiff \| raw \| diff to current
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	bugfix in type_of_aux' which erroneously discard given...	blob \| commitdiff \| raw \| diff to current
2004-11-24	Stefano Zacchiroli	guard get_cooked_obj calls with assert false in case...	blob \| commitdiff \| raw \| diff to current
2004-11-18	Stefano Zacchiroli	use stateful logger so that the ProofChecker daemon...	blob \| commitdiff \| raw \| diff to current
2004-10-22	Andrea Asperti	- ported to typed explicit substitutions	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	removed a useless test on explicit substitutions on...	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...	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