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