Re-indentiation

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 656955808d5abaa231668c99ede556c9325627ac..6664a5b9781cf0b06bb465c78f9f017558d6c522 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -506,15 +506,13 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
       match NCicReduction.whd ~subst context ty_he with 
       | C.Prod (_,s,t) ->
           let metasenv, subst, arg, _ = 
-            typeof rdb ~localise 
-              metasenv subst context arg (Some s) in
+            typeof rdb ~localise metasenv subst context arg (Some s) in
           let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
           aux metasenv subst (arg :: args_so_far) he t tl
       | C.Meta _
       | C.Appl (C.Meta _ :: _) as t ->
           let metasenv, subst, arg, ty_arg = 
-            typeof rdb ~localise 
-              metasenv subst context arg None in
+            typeof rdb ~localise metasenv subst context arg None in
           let name = guess_name subst context ty_arg in
           let metasenv, _, meta, _ = 
             NCicMetaSubst.mk_meta metasenv 
@@ -523,8 +521,7 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
           let flex_prod = C.Prod (name, ty_arg, meta) in
           (* next line grants that ty_args is a type *)
           let metasenv,subst, flex_prod, _ =
-           typeof rdb ~localise metasenv subst
-            context flex_prod None in
+           typeof rdb ~localise metasenv subst context flex_prod None in
 (*
           pp (lazy ( "UNIFICATION in CTX:\n"^ 
             NCicPp.ppcontext ~metasenv ~subst context