From 3594cdffdc6941ed86fef264a681e5db417c5d8a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 13 Feb 2008 16:00:16 +0000 Subject: [PATCH] reordered cases --- helm/software/components/ng_kernel/nCicSubstitution.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml index 67bada949..4f5e25ecc 100644 --- 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 -- 2.39.2