Fixes Trace.v

guarded/Trace.v

@@ -1,6 +1,6 @@
 From MetaCoq.Utils Require Import MCUtils.
 From MetaCoq.Guarded Require Import Except.
-(* Require Import MetaCoq.Guarded.Except. *)
+Require Import List String.
 
 (** Trace Monad built on top of the exception monad for easier debugging. *)
 (** Provides means to limit the number of binds until timeout and to add trace information *)
@@ -13,16 +13,18 @@ Section trace.
   Context (timeout : Y).
 
   Definition trace_info := string.
+  Open Scope type_scope.
   Definition TraceM A :=  bool (* timeout *)
                         * nat (* number of steps on the clock *)
                         * list trace_info (* trace *)
-                        * excOn Y A. (* error monad *)
-
+                        * excOn Y A.
+
+  Open Scope nat_scope.
   (* max steps handling is not totally accurate as we cannot pass the current number of steps into the function in bind, but anyways *)
   Instance trace_monad : Monad TraceM :=
     {|
       ret := fun T t => (false, 0, [], ret t);
-      bind := fun T U x f =>
+      bind := fun T U x f => 
         match x with
         | (b, s, t, e) =>
             if b then (b, s, t, raise timeout) else
@@ -31,7 +33,7 @@ Section trace.
                 match f e with
                 | (b', s', t', e') =>
                     let s'' := 1 + s' + s in
-                    if b || Nat.leb max_steps s'' then (true, s'', t' ++ t, raise timeout)
+                    if (orb b (Nat.leb max_steps s'')) then (true, s'', t' ++ t, raise timeout)
                       else (false, s'', t' ++ t, e')
                 end
             | inr err => (false, s, t, inr err)
@@ -113,6 +115,7 @@ Module example.
   Instance: Monad (@TraceM err) := @trace_monad max_steps err TimeoutErr.
   Notation "'trc' A" := (@TraceM err A) (at level 100).
 
+  Open Scope string_scope.
   Definition test : trc unit :=
     trace "test";;
     raise $ OtherErr "s".

guarded/_CoqProject

@@ -1,5 +1,5 @@
 # TODO: adapt to your location
--R ../common/theories MetaCoq.Common
+# -R ../common/theories MetaCoq.Common
 -R . MetaCoq.Guarded