(* =================================== paramod =========================== *)
let auto_paramod ~params:(l,_) status goal =
+ let l = match l with
+ | None -> raise (Error (lazy "no proof found",None))
+ | Some l -> l in
let gty = get_goalty status goal in
let n,h,metasenv,subst,o = status#obj in
let status,t = term_of_cic_term status gty (ctx_of gty) in