- | l1 -> NCic.Appl l1)
- | NCic.Prod (n,s,t) as orig ->
- let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in
- if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1)
- | NCic.Lambda (n,s,t) as orig ->
- let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in
- if t1 == t && s1 == s then orig else NCic.Lambda (n,s1,t1)
- | NCic.LetIn (n,ty,t,b) as orig ->
+ | l1 -> C.Appl l1)
+ | C.Prod (n,s,t) as orig ->
+ let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in
+ if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
+ | C.Lambda (n,s,t) as orig ->
+ let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in
+ if t1 == t && s1 == s then orig else C.Lambda (n,s1,t1)
+ | C.LetIn (n,ty,t,b) as orig ->