X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=5df06d28d001cdfbc0d74a84e15fbbc2f5f1b91c;hb=74c6905907b0bca229366d52450e2a6982b5b8be;hp=b2003d1d72ed599d35152b25aab2e0d334db33ab;hpb=c4a52e72946988c53d187938fa8c3f6fe7ccbaaa;p=helm.git

diff --git a/matita/components/ng_kernel/nCicUntrusted.ml b/matita/components/ng_kernel/nCicUntrusted.ml
index b2003d1d7..5df06d28d 100644
--- a/matita/components/ng_kernel/nCicUntrusted.ml
+++ b/matita/components/ng_kernel/nCicUntrusted.ml
@@ -209,8 +209,12 @@ let apply_subst status ?(fix_projections=false) subst context t =
                    apply_subst subst () (NCicSubstitution.lift status n t)) l))))
   | t -> NCicUtils.map status (fun _ () -> ()) () (apply_subst subst) t
  in
- (if fix_projections then fire_projection_redex status () else fun x -> x)
-    (clean_or_fix_dependent_abstrations status context (apply_subst subst () t))
+  let t = apply_subst subst () t in
+  let t = clean_or_fix_dependent_abstrations status context t in
+  if fix_projections then
+   fire_projection_redex status () t
+  else
+   t
 ;;
 
 let apply_subst_context status ~fix_projections subst context =
@@ -265,7 +269,7 @@ let rec replace_in_subst i f = function
 ;;
           
 let set_kind newkind attrs = 
-  newkind :: List.filter (fun x -> not (is_kind x)) attrs 
+  (newkind :> NCic.meta_attr) :: List.filter (fun x -> not (is_kind x)) attrs 
 ;;
 
 let max_kind k1 k2 =