Merge pull request #3367 from FStarLang/mtzguido-patch-1

Math.Lemmas: remove needless include in fsti
FStarLang · Jul 21, 2024 · e5cef6f · e5cef6f
2 parents fa18fde + 5e59dc3
commit e5cef6f
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/ulib/FStar.Math.Lemmas.fsti b/ulib/FStar.Math.Lemmas.fsti
@@ -16,7 +16,6 @@
 module FStar.Math.Lemmas
 
 open FStar.Mul
-open FStar.Math.Lib
 
 (* Lemma: definition of Euclidean division *)
 val euclidean_div_axiom: a:int -> b:pos -> Lemma