aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2021-07-07 09:24:33 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2021-07-07 09:24:33 +0200
commitfa531ff0ef33557d38584f03126caea9507a5a67 (patch)
tree4ecd85ec5b4a6fcc09bee725f7c78c192965c95a
parent953715b06c502b51fddc6598f810ff4752621481 (diff)
downloadsmtcoq-fa531ff0ef33557d38584f03126caea9507a5a67.tar.gz
smtcoq-fa531ff0ef33557d38584f03126caea9507a5a67.zip
Ring must be imported
-rw-r--r--src/State.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/State.v b/src/State.v
index dca62e3..16868b7 100644
--- a/src/State.v
+++ b/src/State.v
@@ -10,7 +10,7 @@
(**************************************************************************)
-Require Import List Bool Int63 Psatz Ring63 PArray Omega Misc.
+Require Import List Bool Int63 Psatz Ring63 PArray Omega Misc Ring.
(* Require Import AxiomesInt. *)