]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7845d9d) | patch
:-(
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
tree6e7af4826bd9d8d22a8b67245f9ac89e85d052d4tree | snapshot
parent7845d9d0221d94418beecf3d7c3aed3efb2af7fccommit | diff
:-(
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 diff | blob | history
helm/software/components/cic/deannotate.ml diff | blob | history
helm/software/components/cic/deannotate.mli diff | blob | history
helm/software/components/cic_proof_checking/cicSubstitution.ml diff | blob | history
helm/software/components/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.