]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cca0413) | patch
1. a simplified version of check_allowed_sort_elimination is now exported
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 3 Nov 2005 13:47:36 +0000 (13:47 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 3 Nov 2005 13:47:36 +0000 (13:47 +0000)
commit4f1fda223f9b565267054361f0ec9bdedb86fe6a
tree3f8cc73f148cffc45a1bd60d54732d29e611c268tree | snapshot
parentcca04138889cd0dbafb669a5c3fd8abe424d699ecommit | diff
1. a simplified version of check_allowed_sort_elimination is now exported
   from CicTypeChecker to be used in CicElim :-|
2. check_allowed_sort_elimination fixed w.r.t. the case Prop unit vs *
helm/ocaml/cic_proof_checking/cicElim.ml diff | blob | history
helm/ocaml/cic_proof_checking/cicElim.mli diff | blob | history
helm/ocaml/cic_proof_checking/cicTypeChecker.ml diff | blob | history
helm/ocaml/cic_proof_checking/cicTypeChecker.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.