blob: 8ff5837bb42257b68511c507c8899301fae677d6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Declare ML Module "ltac2_plugin".
Global Set Default Proof Mode "Ltac2".
(** Primitive types *)
Ltac2 Type int.
Ltac2 Type string.
Ltac2 Type char.
Ltac2 Type evar.
Ltac2 Type constr.
Ltac2 Type ident.
Ltac2 Type message.
Ltac2 Type exn := [ .. ].
Ltac2 Type 'a array.
(** Pervasive types *)
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. *)
|
