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/Message.v | |
| parent | fbfe239730bd5069026ae4e5356e93d3f3bfcb53 (diff) | |
Adding a few primitive functions.
Diffstat (limited to 'theories/Message.v')
| -rw-r--r-- | theories/Message.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Message.v b/theories/Message.v index b2159612cb..45f4b221db 100644 --- a/theories/Message.v +++ b/theories/Message.v @@ -14,6 +14,8 @@ Ltac2 @ external of_string : string -> message := "ltac2" "message_of_string". Ltac2 @ external of_int : int -> message := "ltac2" "message_of_int". +Ltac2 @ external of_ident : ident -> message := "ltac2" "message_of_ident". + Ltac2 @ external of_constr : constr -> message := "ltac2" "message_of_constr". (** Panics if there is more than one goal under focus. *) |