wip

Deducteam · Nov 29, 2024 · 737af00 · 737af00
1 parent 2241b23
commit 737af00
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git a/HOLLight.v b/HOLLight.v
@@ -1,18 +1,17 @@
-Require Export HOLLight_Real.HOLLight_Real.
-Require Import Coq.Logic.ClassicalEpsilon.
-
 (*****************************************************************************)
 (* Proof that Coq R is a fourcolor.model of real numbers. *)
 (*****************************************************************************)
 
-Require Export Rbase Rdefinitions Rbasic_fun.
+Require Import HOLLight_Real.HOLLight_Real Rbase Rdefinitions Rbasic_fun.
 
 Open Scope R_scope.
 
 Definition R' := {| type := R; el := 0%R |}.
 
 Canonical R'.
 
+Require Import Coq.Logic.ClassicalEpsilon.
+
 Definition Rsup : (R -> Prop) -> R.
 Proof.
   intro E. case (excluded_middle_informative (bound E)); intro h.

diff --git a/add-real b/add-real
@@ -2,7 +2,7 @@
 
 for f in `find . -name \*.v`
 do
-    if grep -q ': R[)}]' $f
+    if grep -m 1 -q ' R[ )},]' $f
     then
         echo $f
         sed -i -e 's/Require Import HOLLight_Real.HOLLight_Real HOLLight\.$/Require Import HOLLight_Real.HOLLight_Real HOLLight Rdefinitions./' $f