diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md | 4 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_print.ml | 9 |
2 files changed, 9 insertions, 4 deletions
diff --git a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md new file mode 100644 index 0000000000..e0573a2c74 --- /dev/null +++ b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md @@ -0,0 +1,4 @@ +- Internal definitions generated by abstract-like tactics are now inlined + inside universe Qed-terminated polymorphic definitions, similarly to what + happens for their monomorphic counterparts, + (`#10439 <https://github.com/coq/coq/pull/10439>`_, by Pierre-Marie Pédrot). 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 |