Update examples/example_abs_evars.v

LPCIC · Oct 9, 2023 · 489f888 · 489f888
1 parent f41cdc3
commit 489f888
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/examples/example_abs_evars.v b/examples/example_abs_evars.v
@@ -88,7 +88,7 @@ solve (goal _ _ _ _ [trm T] as G) GL :-
 solve (goal _ _ T _ [] as G) GL :-
   std.assert! (abs-evars T ClosedT N) "closure fails",
   coq.mk-app {{ (fun x : lp:ClosedT => x) _ }} {coq.mk-n-holes N} R,
-  std.spy (refine R G GL).
+refine R G GL.
 
 }}.
 Elpi Typecheck.