reordered cases

[helm.git] / helm / software / components / ng_kernel / nCicSubstitution.ml

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 48e96709c47c4943c7bb229675deb1e69285a850..4f5e25ecce91be0764fc841ee5bf423bdea7a317 100644 (file)
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -27,17 +27,6 @@
 
 let debug_print = fun _ -> ();;
 
-(* to be moved in cic util *)
-let expand_local_context = function
-  | NCic.Irl len -> 
-      let rec aux acc = function 
-        | 0 -> acc
-        | n -> aux (NCic.Rel n::acc) (n-1)
-      in
-       aux [] len
-  | NCic.Ctx lctx -> lctx
-;;
-
 let lift_from k n =
  let rec liftaux k = function
     | NCic.Const _ 
@@ -48,7 +37,7 @@ let lift_from k n =
     | NCic.Meta (i,(m,l)) when k <= m -> NCic.Meta (i,(m+n,l))
     | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t
     | NCic.Meta (i,(m,l)) -> 
-       let lctx = expand_local_context l in
+       let lctx = NCicUtils.expand_local_context l in
        NCic.Meta (i, (m, NCic.Ctx (List.map (liftaux (k-m)) lctx)))
     | NCic.Implicit _ -> (* was the identity *) assert false
     | NCic.Prod (n,s,t) -> NCic.Prod (n, liftaux k s, liftaux (k+1) t)
@@ -75,6 +64,8 @@ let lift ?(from=1) n t =
 let rec psubst ?(avoid_beta_redexes=false) delift lift_args args = 
  let nargs = List.length args in
  let rec substaux k = function
+    | NCic.Sort _ 
+    | NCic.Const _ as t -> t
     | NCic.Rel n as t ->
        (match n with
        | n when n >= (k+nargs) -> if delift then NCic.Rel (n - nargs) else t
@@ -85,11 +76,10 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args args =
     | NCic.Meta (_,(m,_)) as t when m >= k + nargs - 1 -> t
     | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t
     | NCic.Meta (i,(m,l)) -> 
-       let lctx = expand_local_context l in
+       let lctx = NCicUtils.expand_local_context l in
        (* 1-nargs < k-m, when <= 0 is still reasonable because we will
         * substitute args[ k-m ... k-m+nargs-1 > 0 ] *)
        NCic.Meta (i,(m, NCic.Ctx (List.map (substaux (k-m)) lctx)))
-    | NCic.Sort _ as t -> t
     | NCic.Implicit _ -> assert false (* was identity *)
     | NCic.Prod (n,s,t) -> NCic.Prod (n, substaux k s, substaux (k + 1) t)
     | NCic.Lambda (n,s,t) -> NCic.Lambda (n, substaux k s, substaux (k + 1) t)
@@ -109,7 +99,6 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args args =
        let tl = List.map (substaux k) tl in
        avoid (substaux k he) tl
     | NCic.Appl _ -> assert false
-    | NCic.Const _ as t -> t
     | NCic.Match (r,outt,t,pl) ->
        NCic.Match (r,substaux k outt, substaux k t, List.map (substaux k) pl)
  in