diff options
Diffstat (limited to 'plugins/romega/const_omega.mli')
| -rw-r--r-- | plugins/romega/const_omega.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index 1c67af806..2901cc028 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -116,6 +116,8 @@ val do_seq : Term.constr -> Term.constr -> Term.constr val do_list : Term.constr list -> Term.constr val mk_nat : int -> Term.constr +val mk_N : int -> Term.constr + (** Precondition: the type of the list is in Set *) val mk_list : Term.constr -> Term.constr list -> Term.constr val mk_plist : Term.types list -> Term.types |