aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin
diff options
context:
space:
mode:
authorMatej Kosik2016-09-23 15:12:23 +0200
committerMatej Kosik2016-09-23 15:12:23 +0200
commit489d80b737ee5f3a2f936abbf2d9bd441d4ef124 (patch)
treeb13f2021391211dc716f48a0122d18a5433ee6cf /mathcomp/ssreflect/plugin
parentd3a954f8910a46664d0cf3ad30e94e555392c2e6 (diff)
FIX: compilation wrt. commit 9c35248 on Coq trunk branch.
Diffstat (limited to 'mathcomp/ssreflect/plugin')
-rw-r--r--mathcomp/ssreflect/plugin/trunk/ssreflect.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index 1250f7e..5fe1ea5 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 Constrarg
+open Stdarg
open Term
open Vars
open Context