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

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

2005-09-21	Claudio Sacerdoti...	More debug_print made lazy.	blob \| commitdiff \| raw
2005-06-09	Claudio Sacerdoti...	CicSubstitution.delift ==> CicMetaSubst.delift_rels	blob \| commitdiff \| raw \| diff to current
2005-06-09	Claudio Sacerdoti...	Exception raised by delift changed:	blob \| commitdiff \| raw \| diff to current
2005-05-31	Enrico Tassi	implemented normalize (used in new_metasenv_for_apply)	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-31	Enrico Tassi	added delift	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
2005-01-05	Stefano Zacchiroli	exported lift_from	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-24	Stefano Zacchiroli	use get_obj instead of get_cooked_obj in order to retri...	blob \| commitdiff \| raw \| diff to current
2004-02-06	Stefano Zacchiroli	added annotations to Cic.Implicit	blob \| commitdiff \| raw \| diff to current
2003-12-17	Claudio Sacerdoti...	* Reindentation	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-04-16	Claudio Sacerdoti...	Invariant enforced: no Appl of another Appl.	blob \| commitdiff \| raw \| diff to current
2001-12-04	Claudio Sacerdoti...	lift 0 was just a very heavy implementation of the...	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