match hyps_pat with
[] -> None,true,(fun ~term _ -> P.exact_tac term),concl_pat,gty
| [name,pat] ->
- 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
+ let arg,gty = ProofEngineHelpers.find_hyp name context in
let dummy = "dummy" in
Some arg,false,
(fun ~term typ ->