diff options
Diffstat (limited to 'common/Errors.v')
| -rw-r--r-- | common/Errors.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/common/Errors.v b/common/Errors.v index 36e70c5..a70ea6e 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -30,7 +30,8 @@ Set Implicit Arguments. Inductive errcode: Type := | MSG: string -> errcode - | CTX: positive -> errcode. + | CTX: positive -> errcode (* a top-level identifier *) + | CTXL: positive -> errcode. (* an encoded local identifier *) Definition errmsg: Type := list errcode. |