Skip to content

Commit

Permalink
Compatibility with coq-interval.4.7.0
Browse files Browse the repository at this point in the history
The relevant change in coq-interval is
```diff
diff --git a/src/Tactic.v b/src/Tactic.v
index 6aec7b6..de2181d 100644
--- a/src/Tactic.v
+++ b/src/Tactic.v
@@ -53,7 +53,7 @@ Module I1 := FloatIntervalFull F.
 Module IT1 := IntegralTacticAux F I1.
 Module PT1 := PlotTacticAux F I1.
 Module RT1 := RootTacticAux F I1.
-Module I2 := FloatIntervalFull Tactic_float.Float.
+Module I2 := Tactic_float.Interval.
 Module IT2 := IntegralTacticAux Tactic_float.Float I2.
 Module PT2 := PlotTacticAux Tactic_float.Float I2.
 Module RT2 := RootTacticAux Tactic_float.Float I2.
```

I have no idea what I'm doing, but the import seems to be unused?
  • Loading branch information
JasonGross committed Aug 6, 2023
1 parent 202bfb0 commit 90d5a0c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion vcfloat/Prune.v
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Require Import Setoid.

Import Coq.Lists.List ListNotations.
Import Tree. (* must import this _after_ List *)
Import Interval Private Interval_helper I2 IT2.IH I2.T Xreal Eval.Reify.
Import Interval Private Interval_helper I2 IT2.IH Xreal Eval.Reify.

Import Basic.
Import Bool.
Expand Down

0 comments on commit 90d5a0c

Please sign in to comment.