(match metasenv with
None ->
Cic.Constant
- (id, Some (proof2cic deannotate bo), deannotate ty, params)
+ (id, Some (proof2cic deannotate bo), deannotate ty, params, [])
| Some metasenv' ->
let metasenv'' =
List.map
) metasenv'
in
Cic.CurrentProof
- (id, metasenv'', proof2cic deannotate bo, deannotate ty, params))
+ (id, metasenv'', proof2cic deannotate bo, deannotate ty, params,
+ []))
| _ -> raise ToDo
;;