Cic.Sort(Cic.Prop))
else
Cic.Sort Cic.Prop
- | _ -> assert false
;;
(* created vars is empty at the beginning *)
if List.length (list_of_prod arity) = (nleft + 1) then
None
else
- begin
+ try
let arity_l = cut_last (list_of_prod arity) in
let rightparam_tys = cut_first nleft arity_l in
let theorem = build_theorem rightparam_tys arity_l arity cons_list
Some
(inversor_uri,
Cic.Constant (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
- end
+ with
+ Inversion.EqualityNotDefinedYet -> None
;;
let init () = ();;