]> matita.cs.unibo.it Git - helm.git/commitdiff
Identity change, improves readability.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 2 Feb 2013 00:30:45 +0000 (00:30 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 2 Feb 2013 00:30:45 +0000 (00:30 +0000)
matita/components/ng_kernel/nCicUntrusted.ml

index b2003d1d72ed599d35152b25aab2e0d334db33ab..ba5ad9f5ad6480e744b9ea9bb53a0a3840721412 100644 (file)
@@ -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 =