aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/auto_ind_decl.ml
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-21 20:04:58 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:39:25 +0200
commit02d2f34e5c84f0169e884c07054a6fbfef9f365c (patch)
tree5e55f22c5b20dcf694c00741a69dae6f1d993267 /vernac/auto_ind_decl.ml
parent95239fa33c5da60080833dabc3ced246680dfdf9 (diff)
Remove some unused values and types
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 *)