is this the right uctx for inductive?

LPCIC · Jul 8, 2024 · f4340e1 · f4340e1
1 parent 59c7677
commit f4340e1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -2110,7 +2110,7 @@ Supported attributes:
            | Names.Name id -> Dumpglob.dump_definition (lid_of id) false "proj"
            | Names.Anonymous -> ()) names;
       end;
-     None,state, !: ind, []))),
+     Some uctx,state, !: ind, []))),
   DocAbove);
 
   LPDoc "Interactive module construction";