diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/declare.ml b/library/declare.ml index 58ad1f00f..63a2c03a7 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -183,7 +183,7 @@ let declare_constant ?(internal = UserVerbose) id (cd,kind) = (** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = - list_iter_i (fun i {mind_entry_consnames=lc} -> + List.iter_i (fun i {mind_entry_consnames=lc} -> Notation.declare_ref_arguments_scope (IndRef (kn,i)); for j=1 to List.length lc do Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); |