]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed in the computation of the disambiguation domain of a let...rec.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Feb 2007 18:47:05 +0000 (18:47 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Feb 2007 18:47:05 +0000 (18:47 +0000)
helm/software/components/cic_disambiguation/disambiguate.ml

index 5c198cb5962bf06bef7850892ba384ffe2c35618..ac26903b184165569272747fd10a1219ded135c8 100644 (file)
@@ -684,7 +684,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                   CicNotationUtil.cic_name_of_name var :: context,
                   domain_of_term_option ~loc ~context ty @ res)
                 (add_defs context,[]) params))
-            @ domain_of_term_option ~loc ~context typ
+            @ domain_of_term_option ~loc ~context:context' typ
             @ domain_of_term ~loc ~context:context' body
           ) [] defs
       in