diff options
| author | Pierre Roux | 2019-05-10 16:48:40 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-05-10 16:48:40 +0200 |
| commit | a17626eb716b8a7b0ae5c1387f485223ba1c2de5 (patch) | |
| tree | c6cf0c33d1c42f4e121e4a4badd41922858483ea /user-contrib/Ltac2/Init.v | |
| parent | f913913a6a1b1e01d154d0c9af3b3807459b0b9f (diff) | |
[ltac2] Add primitive integers
Diffstat (limited to 'user-contrib/Ltac2/Init.v')
| -rw-r--r-- | user-contrib/Ltac2/Init.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 16e7d7a6f9..dc1690bdfb 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -14,6 +14,7 @@ Ltac2 Type int. Ltac2 Type string. Ltac2 Type char. Ltac2 Type ident. +Ltac2 Type uint63. (** Constr-specific built-in types *) Ltac2 Type meta. |