diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 5 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 4 | ||||
| -rw-r--r-- | parsing/prettyp.mli | 2 |
5 files changed, 9 insertions, 9 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index a8f46a12b1..648bb28297 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -191,7 +191,7 @@ GEXTEND Gram | IDENT "Coercions" -> PrintCoercions | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> PrintCoercionPaths (s,t) - | IDENT "Canonical"; IDENT "Structures" -> PrintCanonicalStructures + | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions | IDENT "Tables" -> PrintTables | "Proof"; qid = global -> PrintOpaqueName qid | IDENT "Hint" -> PrintHintGoal diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 26a38e381e..603abd73a7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -404,9 +404,8 @@ GEXTEND Gram | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = Ast.coerce_global_to_id qid in VernacDefinition - ((Global,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook) - (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed - (they were unused and undocumented) *) + ((Global,CanonicalStructure),(dummy_loc,s),d, + (fun _ -> Recordops.declare_canonical_structure)) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index 5b0350f82e..a32e32538d 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -402,7 +402,8 @@ GEXTEND Gram | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = Ast.coerce_global_to_id qid in VernacDefinition - ((Global,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook) + ((Global,CanonicalStructure),(dummy_loc,s),d, + (fun _ -> Recordops.declare_canonical_structure)) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> @@ -579,7 +580,7 @@ GEXTEND Gram | IDENT "Coercions" -> PrintCoercions | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> PrintCoercionPaths (s,t) - | IDENT "Canonical"; IDENT "Structures" -> PrintCanonicalStructures + | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions | IDENT "Tables" -> PrintTables (* Obsolete: was used for cooking V6.3 recipes ?? | IDENT "Proof"; qid = global -> PrintOpaqueName qid diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index a358301e5b..eded75be9d 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -628,9 +628,9 @@ let print_path_between cls clt = in print_path ((i,j),p) -let print_canonical_structures () = +let print_canonical_projections () = prlist_with_sep pr_fnl (fun ((r1,r2),o) -> pr_global r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ prterm o.o_DEF ++ str " )") - (canonical_structures ()) + (canonical_projections ()) (*************************************************************************) diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 20429cd3d9..4c52420d02 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -57,7 +57,7 @@ val print_graph : unit -> std_ppcmds val print_classes : unit -> std_ppcmds val print_coercions : unit -> std_ppcmds val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds -val print_canonical_structures : unit -> std_ppcmds +val print_canonical_projections : unit -> std_ppcmds val inspect : int -> std_ppcmds |