From 41cea8603b35a1af405650d8a2b9aaa89a445367 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Jul 2017 19:00:29 +0200
Subject: Adding a few primitive functions.

---
 theories/Init.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'theories/Init.v')

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 ].
-- 
cgit v1.2.3