From 1144eafda5f046c21ceda807f4b5659b3e74147d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 29 Sep 2009 17:01:28 +0000 Subject: [PATCH] Re-indentiation --- helm/software/components/ng_refiner/nCicRefiner.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 656955808..6664a5b97 100644 --- 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 -- 2.39.2