From 75f0abfa4979cd0050399093fd07e7c952de49b4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 24 Sep 2016 13:33:28 +0200
Subject: Fix ML compilation after Ltac refactoring.

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index 5fe1ea5..398c0c3 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -29,7 +29,7 @@ open Pcoq.Prim
 open Pcoq.Constr
 open Genarg
 open Stdarg
-open Stdarg
+open Tacarg
 open Term
 open Vars
 open Context
@@ -45,6 +45,7 @@ open Coqlib
 open Glob_term
 open Util
 open Evd
+open Proofview.Notations
 open Sigma.Notations
 open Extend
 open Goptions
-- 
cgit v1.2.3