X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=8dc94e9e462f689803c44c346adf18f460a417a8;hb=d6ba7f4b8fbd98f2f1c848857022ef5fba80db53;hp=56ec069d2c77bb7d30eff3773073908bdc01b6ff;hpb=8049c166a37789d7a1b1ca1c3a1174712bbf87ba;p=helm.git

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