From 735ab0a7d2f7afaed0695e014034f4b2d6e287c8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Dec 2016 08:09:54 +0100
Subject: Stdlib functions now return Ltac2 exceptions.

---
 Init.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'Init.v')

diff --git a/Init.v b/Init.v
index 322f275346..8ff5837bb4 100644
--- a/Init.v
+++ b/Init.v
@@ -30,3 +30,17 @@ Ltac2 Type 'a option := [ None | Some ('a) ].
 Ltac2 Type 'a ref := { mutable contents : 'a }.
 
 Ltac2 Type bool := [ true | false ].
+
+(** Pervasive exceptions *)
+
+Ltac2 Type exn ::= [ Out_of_bounds ].
+(** Used for bound checking, e.g. with String and Array. *)
+
+Ltac2 Type exn ::= [ Not_focussed ].
+(** In Ltac2, the notion of "current environment" only makes sense when there is
+    at most one goal under focus. Contrarily to Ltac1, instead of dynamically
+    focussing when we need it, we raise this non-backtracking error when it does
+    not make sense. *)
+
+Ltac2 Type exn ::= [ Not_found ].
+(** Used when something is missing. *)
-- 
cgit v1.2.3