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/cicEnvironment.ml

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

2005-10-25	Claudio Sacerdoti...	Every exception that used to have type string is now...	blob \| commitdiff \| raw
2005-09-23	Enrico Tassi	added universes list handling	blob \| commitdiff \| raw \| diff to current
2005-09-21	Claudio Sacerdoti...	More debug_print made lazy.	blob \| commitdiff \| raw \| diff to current
2005-07-22	Andrea Asperti	CicEnvironment.remove did not remove the object from...	blob \| commitdiff \| raw \| diff to current
2005-07-05	Stefano Zacchiroli	ported to new getter interface	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-05-27	Enrico Tassi	removed debug prerr_endline	blob \| commitdiff \| raw \| diff to current
2005-05-05	Stefano Zacchiroli	- ported to new CicParser interface which requires...	blob \| commitdiff \| raw \| diff to current
2005-04-29	Enrico Tassi	added more assertions on universes when loaded from...	blob \| commitdiff \| raw \| diff to current
2005-04-29	Enrico Tassi	added parsing time benchmark	blob \| commitdiff \| raw \| diff to current
2005-04-29	Stefano Zacchiroli	fix (ask Enrico :-)	blob \| commitdiff \| raw \| diff to current
2005-04-29	Stefano Zacchiroli	uses CicUniv new assertions	blob \| commitdiff \| raw \| diff to current
2005-04-27	Stefano Zacchiroli	added re-hash-consing of URIs embedded in universes	blob \| commitdiff \| raw \| diff to current
2005-03-11	Stefano Zacchiroli	Bugfix in restore_from_channel, before this fix hashtab...	blob \| commitdiff \| raw \| diff to current
2005-02-14	Enrico Tassi	Fixed remove operation and get_obj (that now correctly...	blob \| commitdiff \| raw \| diff to current
2005-02-10	Stefano Zacchiroli	renaming "remove_term" -> "remove_obj"	blob \| commitdiff \| raw \| diff to current
2005-02-08	Stefano Zacchiroli	added a missing unchecked_to_frozen (fixes a Not_found...	blob \| commitdiff \| raw \| diff to current
2005-01-25	Enrico Tassi	added list_obj and list_uri	blob \| commitdiff \| raw \| diff to current
2005-01-24	Stefano Zacchiroli	- renamed Term_not_found exception (useless) with Objec...	blob \| commitdiff \| raw \| diff to current
2005-01-21	Stefano Zacchiroli	added attributes support	blob \| commitdiff \| raw \| diff to current
2005-01-18	Enrico Tassi	fixed comments	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-18	Stefano Zacchiroli	added set_trust to externally set the trust function...	blob \| commitdiff \| raw \| diff to current
2004-10-22	Stefano Zacchiroli	- ported to new getter API	blob \| commitdiff \| raw \| diff to current
2004-10-22	Andrea Asperti	cleanup temp files on parser failure	blob \| commitdiff \| raw \| diff to current
2004-06-01	Enrico Tassi	new universes implementation	blob \| commitdiff \| raw \| diff to current
2004-04-05	Andrea Asperti	Added a new function in_cache to cicEnvironemt. It...	blob \| commitdiff \| raw \| diff to current
2004-02-11	Stefano Zacchiroli	new logger	blob \| commitdiff \| raw \| diff to current
2004-02-06	Stefano Zacchiroli	added annotations to Cic.Implicit	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-09-13	Stefano Zacchiroli	added support for dump/restore/clear proof checker...	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-01-29	Claudio Sacerdoti...	Ported to ocaml-3.04	blob \| commitdiff \| raw \| diff to current
2001-12-13	Claudio Sacerdoti...	The hash-table used in the implementation was of "type"	blob \| commitdiff \| raw \| diff to current
2001-12-13	Claudio Sacerdoti...	New architecture for the environment.	blob \| commitdiff \| raw \| diff to current
2001-12-03	Claudio Sacerdoti...	* Major code cleanup.	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