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

2001-12-07	Claudio Sacerdoti...	Bug partially fixed: the branch of a case of type Prod...	blob \| commitdiff \| raw
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.