diff options
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.mli')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.mli b/doc/plugin_tutorial/tuto1/src/simple_declare.mli index fd74e81526..c55b36742f 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.mli +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.mli @@ -1,5 +1,4 @@ open Names -open EConstr -val packed_declare_definition : - poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit +val declare_definition : + poly:bool -> Id.t -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t |