diff options
Diffstat (limited to 'doc/plugin_tutorial')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_print.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml index ba989b1bac..88afec14d5 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -2,14 +2,15 @@ type constr is given in the coq-dpdgraph plugin. *) let simple_body_access gref = + let open Names.GlobRef in match gref with - | Globnames.VarRef _ -> + | VarRef _ -> failwith "variables are not covered in this example" - | Globnames.IndRef _ -> + | IndRef _ -> failwith "inductive types are not covered in this example" - | Globnames.ConstructRef _ -> + | ConstructRef _ -> failwith "constructors are not covered in this example" - | Globnames.ConstRef cst -> + | ConstRef cst -> let cb = Environ.lookup_constant cst (Global.env()) in match Global.body_of_constant_body Library.indirect_accessor cb with | Some(e, _, _) -> EConstr.of_constr e |