matita.cs.unibo.it Git - helm.git/history - helm/ocaml/cic_unification/cicMkImplicit.ml

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

projects / helm.git / history

summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next

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

2005-06-15	Claudio Sacerdoti...	Big commit and major code clean-up:	blob \| commitdiff \| raw
2005-01-11	Stefano Zacchiroli	added fallback case (assertion failure) for unsupported...	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-04-23	Enrico Tassi	Universes introduction	blob \| commitdiff \| raw \| diff to current
2004-02-11	Claudio Sacerdoti...	Added copyright notice.	blob \| commitdiff \| raw \| diff to current
2004-02-07	Claudio Sacerdoti...	Added mk_implicit_sort.	blob \| commitdiff \| raw \| diff to current
2004-02-06	Claudio Sacerdoti...	sort metavariables are now generated in an empty canoni...	blob \| commitdiff \| raw \| diff to current
2004-02-06	Stefano Zacchiroli	added annotations to Cic.Implicit	blob \| commitdiff \| raw \| diff to current
2004-02-04	Stefano Zacchiroli	removed a debugging message	blob \| commitdiff \| raw \| diff to current
2004-02-03	Claudio Sacerdoti...	cic_mkimplicit' removed (its implementation was wrong...	blob \| commitdiff \| raw \| diff to current
2004-02-03	Claudio Sacerdoti...	Debugging code removed.	blob \| commitdiff \| raw \| diff to current
2004-02-03	Claudio Sacerdoti...	Added an optional parameter to identity_relocation_list...	blob \| commitdiff \| raw \| diff to current
2004-02-02	Stefano Zacchiroli	- bugfix for expand_implicits, return correct term...	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
2004-01-19	Stefano Zacchiroli	added MkImplicit module for meta handling	blob \| commitdiff \| raw \| diff to current

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