aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/auto_ind_decl.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/auto_ind_decl.ml')
-rw-r--r--vernac/auto_ind_decl.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index b9c4c6cc5..015552d68 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -28,8 +28,6 @@ open Proofview.Notations
module RelDecl = Context.Rel.Declaration
-let out_punivs = Univ.out_punivs
-
(**********************************************************************)
(* Generic synthesis of boolean equality *)