aboutsummaryrefslogtreecommitdiff
path: root/tuto1/src/simple_declare.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tuto1/src/simple_declare.mli')
-rw-r--r--tuto1/src/simple_declare.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tuto1/src/simple_declare.mli b/tuto1/src/simple_declare.mli
index 7a28626d88..fd74e81526 100644
--- a/tuto1/src/simple_declare.mli
+++ b/tuto1/src/simple_declare.mli
@@ -2,4 +2,4 @@ open Names
open EConstr
val packed_declare_definition :
- Id.t -> constr Evd.in_evar_universe_context -> unit \ No newline at end of file
+ poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit