From 803c1dbf2de4e4fe1e447a69b9e5c48d19a72f5f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Jun 2019 13:24:05 +0200
Subject: Remove the internal_flag argument from Declare API.

It was never used actually.
---
 vernac/comAssumption.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comAssumption.ml')

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index e791118db2..e91d8b9d3e 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -280,7 +280,7 @@ let context ~poly l =
         let entry = Declare.definition_entry ~univs ~types:t b in
         (Declare.DefinitionEntry entry, IsAssumption Logical)
       in
-      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
+      let cst = Declare.declare_constant id decl in
       let env = Global.env () in
       Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
       status
-- 
cgit v1.2.3