]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3d5c864) | patch
Bug fixed: the current substitution and metasenv were not propagated to the
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 25 Oct 2005 08:22:12 +0000 (08:22 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 25 Oct 2005 08:22:12 +0000 (08:22 +0000)
commitb5b653d8880924fe05233f4eb160a189c8a995b8
tree783dba35b945f488692d8b6adb8f0177a1d0f32atree | snapshot
parent3d5c86473cd2549335e7ee99600b0aaf499ca651commit | diff
Bug fixed: the current substitution and metasenv were not propagated to the
check_allowed_sort_elimination function. As a result:
 1. useless metas were opened by the apply tactic
 2. sometimes unification failed
helm/ocaml/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.