From 6cc40e73879aec50227c9576100a381cc11ade30 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 7 Nov 2018 13:55:14 +0100
Subject: [warnings] Fix couple of warnings related to API..

Changes in declare following @SkySkimmer's advice.
---
 tuto3/src/tuto_tactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tuto3/src')

diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
index cb73a4486b..9818867621 100644
--- a/tuto3/src/tuto_tactic.ml
+++ b/tuto3/src/tuto_tactic.ml
@@ -15,7 +15,7 @@ let collect_constants () =
     let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in
     let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in
     let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in
-    constants := List.map (fun x -> of_constr (constr_of_global x))
+    constants := List.map (fun x -> of_constr (constr_of_monomorphic_global x))
       [gr_H; gr_M; gr_R; gr_P; gr_U];
     !constants
   else
-- 
cgit v1.2.3