- delift_type_wrt_term fixed in many ways

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 58036784f634e8e8427f3c86d4987ac0fce35d0b..f46487aabda862068115d907c62809c7701f4db0 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -242,7 +242,7 @@ let rec typeof rdb
          | Some x -> 
              let m, s, x = 
                NCicUnification.delift_type_wrt_terms 
-                 rdb metasenv subst context x [t]
+               rdb metasenv subst context x [t]
              in
                m, s, Some x
        in