From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 16 Sep 2009 08:32:32 +0000 (+0000)
Subject: The left parameters coming from the constructor types have been refined in a
X-Git-Tag: make_still_working~3463
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d6ba7f4b8fbd98f2f1c848857022ef5fba80db53;p=helm.git

The left parameters coming from the constructor types have been refined in a
longer context. Thus we need to unify them in the longer context (that does not
hurt those coming from the inductive types).
---

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 56ec069d2..8dc94e9e4 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -746,7 +746,7 @@ let typeof_obj
                       "and those of its inductive type"))))
                    else
                     metasenv,subst,item1::context
-                ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev
+                ) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
               with Invalid_argument "List.fold_left2" -> assert false in
              let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in
               (match