summaryrefslogtreecommitdiff
path: root/plugins/firstorder/sequent.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-01-26 16:56:33 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-01-26 16:56:33 +0100
commit164c6861860e6b52818c031f901ffeff91fca16a (patch)
tree4f91d20c890c25915e7b28226c663b94a8cfb0d3 /plugins/firstorder/sequent.mli
parent91dbeab8eef959c3f64960909ca69d4e68c8198d (diff)
Imported Upstream version 8.5upstream/8.5
Diffstat (limited to 'plugins/firstorder/sequent.mli')
-rw-r--r--plugins/firstorder/sequent.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index dc3f05be..06c9251e 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -13,7 +13,7 @@ open Globnames
module OrderedConstr: Set.OrderedType with type t=constr
-module CM: Map.S with type key=constr
+module CM: CSig.MapS with type key=constr
type h_item = global_reference * (int*constr) option