]> matita.cs.unibo.it Git - helm.git/commit
:-(
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 13 Mar 2008 18:48:26 +0000 (18:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 13 Mar 2008 18:48:26 +0000 (18:48 +0000)
commitb699884bb9816aa55f9bd0a2d7bffde4dc03c643
tree6e7af4826bd9d8d22a8b67245f9ac89e85d052d4
parent7845d9d0221d94418beecf3d7c3aed3efb2af7fc
:-(
This commit introduces an hack in deannotate.ml to compute on-the-fly the types
for the body in a LetIn parsed from an XML file. This happens when parsing Coq
files. We should re-export everything from Coq sooner or later.
helm/software/components/cic/cicParser.ml
helm/software/components/cic/deannotate.ml
helm/software/components/cic/deannotate.mli
helm/software/components/cic_proof_checking/cicSubstitution.ml
helm/software/components/cic_proof_checking/cicTypeChecker.ml