| Cic.Prod (Cic.Name n, s, t) ->
PT.Binder (`Forall, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Decl s)::c) t)
- | Cic.LetIn (Cic.Name n, s, t) ->
+ | Cic.LetIn (Cic.Name n, s, ty, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
- aux (Some (Cic.Name n, Cic.Def (s,None))::c) t)
+ aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
| Cic.Meta _ -> PT.Implicit
| Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
| Cic.Sort Cic.Set -> PT.Sort `Set
Auto.revision time size depth
in
let proof_script =
- if List.exists (fun (s,_) -> s = "paramodulation") params then
+ if List.exists (fun (s,_) -> s = "paramodulation") (snd params) then
let proof_term, how_many_lambdas =
Auto.lambda_close ~prefix_name:"orrible_hack_"
proof_term menv cc