reordered cases

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 67bada94989b41a4631158f3f3abd18a190a1541..4f5e25ecce91be0764fc841ee5bf423bdea7a317 100644 (file)
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -64,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
@@ -78,7 +80,6 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args args =
        (* 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)
@@ -98,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