diff options
| author | Maxime Dénès | 2018-12-21 18:01:17 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-22 11:11:34 +0100 |
| commit | 4922d0d6e156338485b48ce3fd34c1179a505083 (patch) | |
| tree | 2562bb8e677ff9afb7d51a8a079ce282c2b844da | |
| parent | b6ac490a583c83096d810c25e89d01fb7d25741f (diff) | |
VernacDeclareClass -> VernacExistingClass
| -rw-r--r-- | stm/vernac_classifier.ml | 2 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 2 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 2 |
5 files changed, 6 insertions, 6 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index b9cc7e5916..bc5c14c9b1 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -160,7 +160,7 @@ let classify_vernac e = | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ | VernacDeclareReduction _ - | VernacDeclareClass _ | VernacExistingInstance _ + | VernacExistingClass _ | VernacExistingInstance _ | VernacRegister _ | VernacNameSectionHypSet _ | VernacDeclareCustomEntry _ diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index b5bc1c8111..0d3617b162 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -695,7 +695,7 @@ GRAMMAR EXTEND Gram let insts = List.map (fun i -> (i, info)) ids in VernacExistingInstance insts } - | IDENT "Existing"; IDENT "Class"; is = global -> { VernacDeclareClass is } + | IDENT "Existing"; IDENT "Class"; is = global -> { VernacExistingClass is } (* Arguments *) | IDENT "Arguments"; qid = smart_global; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 8be43c9495..3a3da8e2d8 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -922,7 +922,7 @@ open Pputils spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts) ) - | VernacDeclareClass id -> + | VernacExistingClass id -> return ( hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id) ) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 28ce619f10..910fb1a916 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1020,7 +1020,7 @@ let vernac_existing_instance ~section_local insts = let glob = not section_local in List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts -let vernac_declare_class id = +let vernac_existing_class id = Record.declare_existing_class (Nametab.global id) (***********) @@ -2231,7 +2231,7 @@ let interp ?proof ~atts ~st c = vernac_instance ~atts abst sup inst props info | VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts - | VernacDeclareClass id -> unsupported_attributes atts; vernac_declare_class id + | VernacExistingClass id -> unsupported_attributes atts; vernac_existing_class id (* Solving *) | VernacSolveExistential (n,c) -> unsupported_attributes atts; vernac_solve_existential n c diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 9b36159073..3eb90f0d30 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -311,7 +311,7 @@ type nonrec vernac_expr = | VernacExistingInstance of (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *) - | VernacDeclareClass of qualid (* inductive or definition name *) + | VernacExistingClass of qualid (* inductive or definition name *) (* Modules and Module Types *) | VernacDeclareModule of bool option * lident * |