- let rec find_hyp n =
- function
- [] -> assert false
- | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
- Cic.Rel n, S.lift n ty
- | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
- | _::tl -> find_hyp (n+1) tl
- in
- let arg,gty = find_hyp 1 context in