]> matita.cs.unibo.it Git - helm.git/commit
Bug fixed in handling of explicit named substitutions: it could happen that
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 3 May 2008 21:31:45 +0000 (21:31 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 3 May 2008 21:31:45 +0000 (21:31 +0000)
commitd344d41028275b6d1451dca8e40a88e33e588389
tree053cadd8c19c622ea3ad27a23e93b5b310a8e553
parentb38be3a054228c22fbe82cc87bc72504b2b42571
Bug fixed in handling of explicit named substitutions: it could happen that
explicit named substitution are merged not in the expected order. This happens
comparing the case of an instantiation inside and outside a (nested) section.
Thus I have added back the re-ordering of the explicit named substitution in
CicSubstitution.subst_vars and in CicReduction.unwind_aux. Moreover, I have
added to CicTypechecker.type_of_aux' the check that verifies if an explicit
named substitution is ordered.
helm/software/components/cic_proof_checking/cicReduction.ml
helm/software/components/cic_proof_checking/cicSubstitution.ml
helm/software/components/cic_proof_checking/cicTypeChecker.ml
helm/software/components/ng_kernel/TEST