From da5bbda84bd22b87a6057175c9d4d2391808e294 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 17:28:26 +0200
Subject: [api] [proof] Move `discharge` type to vernac_ast where it is used.

This seems like the right location, a bit more refactoring should be
possible.
---
 plugins/funind/g_indfun.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index ef9d91c7fa..e20d010c71 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -182,7 +182,7 @@ let is_proof_termination_interactively_checked recsl =
 
 let classify_as_Fixpoint recsl =
  Vernac_classifier.classify_vernac
-    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
+    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(NoDischarge, List.map snd recsl))))
 
 let classify_funind recsl =
   match classify_as_Fixpoint recsl with
-- 
cgit v1.2.3