eat_lambdas and eat_or_subst_lambdas taken out of the big recursion.

In principle, we could move them to nCicUtils. Maybe this should be done.

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 7995f5c8720e5903501b2e5fa22424c0b91182bc..f43c3a592fa769254bc9bd6c7c1a94bbe6786901 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -239,6 +239,30 @@ let does_not_occur ~subst context n nn t =
    with DoesOccur -> false
 ;;
 
+let rec eat_lambdas ~subst ~metasenv context n te =
+  match (n, R.whd ~subst context te) with
+  | (0, _) -> (te, context)
+  | (n, C.Lambda (name,so,ta)) when n > 0 ->
+      eat_lambdas ~subst ~metasenv ((name,(C.Decl so))::context) (n - 1) ta
+   | (n, te) ->
+      raise (AssertFailure (lazy (Printf.sprintf "eat_lambdas (%d, %s)" n 
+        (PP.ppterm ~subst ~metasenv ~context te))))
+;;
+
+let rec eat_or_subst_lambdas ~subst ~metasenv n te to_be_subst args
+     (context, recfuns, x as k)
+=
+  match n, R.whd ~subst context te, to_be_subst, args with
+  | (n, C.Lambda (name,so,ta),true::to_be_subst,arg::args) when n > 0 ->
+      eat_or_subst_lambdas ~subst ~metasenv (n - 1) (S.subst arg ta)
+       to_be_subst args k
+  | (n, C.Lambda (name,so,ta),false::to_be_subst,arg::args) when n > 0 ->
+      eat_or_subst_lambdas ~subst ~metasenv (n - 1) ta to_be_subst args
+       (shift_k (name,(C.Decl so)) k)
+  | (_, te, _, _) -> te, k
+;;
+
+
 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
@@ -699,27 +723,6 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
         i + 1)
     tyl 1)
 
-and eat_lambdas ~subst ~metasenv context n te =
-  match (n, R.whd ~subst context te) with
-  | (0, _) -> (te, context)
-  | (n, C.Lambda (name,so,ta)) when n > 0 ->
-      eat_lambdas ~subst ~metasenv ((name,(C.Decl so))::context) (n - 1) ta
-   | (n, te) ->
-      raise (AssertFailure (lazy (Printf.sprintf "eat_lambdas (%d, %s)" n 
-        (PP.ppterm ~subst ~metasenv ~context te))))
-
-and eat_or_subst_lambdas ~subst ~metasenv n te to_be_subst args
-     (context, recfuns, x as k) 
-=
-  match n, R.whd ~subst context te, to_be_subst, args with
-  | (n, C.Lambda (name,so,ta),true::to_be_subst,arg::args) when n > 0 ->
-      eat_or_subst_lambdas ~subst ~metasenv (n - 1) (S.subst arg ta)
-       to_be_subst args k
-  | (n, C.Lambda (name,so,ta),false::to_be_subst,arg::args) when n > 0 ->
-      eat_or_subst_lambdas ~subst ~metasenv (n - 1) ta to_be_subst args
-       (shift_k (name,(C.Decl so)) k)
-  | (_, te, _, _) -> te, k
-
 and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = 
  let recursor f k t = U.fold shift_k k (fun k () -> f k) () t in
  let rec aux (context, recfuns, x as k) t =