]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3e8f729) | patch
Assert false removed (although conceptually correct).
authorAndrea Asperti <andrea.asperti@unibo.it>
Wed, 20 Jul 2005 07:22:49 +0000 (07:22 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Wed, 20 Jul 2005 07:22:49 +0000 (07:22 +0000)
commit4f179a8afdb2f11e669354f8fca4ffd1b0308bd2
tree50e371ff684d921e8105d865722f0a5e084375fftree | snapshot
parent3e8f729a0e48566f9d1941cad2feec099880665fcommit | diff
Assert false removed (although conceptually correct).
The problem isgenerating names during the refinement of incomplete terms;
the right solution would be to generate names only AFTER refinement.
helm/ocaml/cic_proof_checking/.depend diff | blob | history
helm/ocaml/cic_proof_checking/freshNamesGenerator.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.