diff options
| author | Pierre-Marie Pédrot | 2017-07-24 19:00:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-24 23:50:58 +0200 |
| commit | 41cea8603b35a1af405650d8a2b9aaa89a445367 (patch) | |
| tree | c41d47f9f5582bb0b267e2422195f8206eb7fef2 /theories/Init.v | |
| parent | fbfe239730bd5069026ae4e5356e93d3f3bfcb53 (diff) | |
Adding a few primitive functions.
Diffstat (limited to 'theories/Init.v')
| -rw-r--r-- | theories/Init.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Init.v b/theories/Init.v index 1d2d40f5c0..c0a73576d3 100644 --- a/theories/Init.v +++ b/theories/Init.v @@ -41,6 +41,8 @@ Ltac2 Type 'a ref := { mutable contents : 'a }. Ltac2 Type bool := [ true | false ]. +Ltac2 Type 'a result := [ Val ('a) | Err (exn) ]. + (** Pervasive exceptions *) Ltac2 Type exn ::= [ Out_of_bounds ]. |