let rec aux =
function
Cic.Sort s -> `Sort s
- | Cic.Prod (_,_,t)
- | Cic.Lambda (_,_,t) -> aux t
+ | Cic.Prod (_,_,t) -> aux t
| _ -> `SomethingElse
in
match aux t with
let reserved =
[ "to";
"mod";
- "val"
+ "val";
+ "in";
+ "function"
]
in
function n ->