diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d5366f8c6..b603b28e3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -916,6 +916,15 @@ let _ = | _ -> bad_vernac_args "DEFINITION") let _ = + add "CANONICAL" + (function + | [VARG_QUALID qid] -> + fun () -> + let ref = Nametab.global dummy_loc qid in + Recordobj.objdef_declare ref + | _ -> bad_vernac_args "CANONICAL") + +let _ = add "VARIABLE" (function | [VARG_STRING kind; VARG_BINDERLIST slcl] -> |