aboutsummaryrefslogtreecommitdiffstats
path: root/src/euf/Euf.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/euf/Euf.v')
-rw-r--r--src/euf/Euf.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/euf/Euf.v b/src/euf/Euf.v
index 9b86bf3..e3d73f6 100644
--- a/src/euf/Euf.v
+++ b/src/euf/Euf.v
@@ -36,7 +36,7 @@ Section certif.
end
| _ => C._true
end.
- Register get_eq as PrimInline.
+ (* Register get_eq as PrimInline. *)
Fixpoint check_trans_aux (t1 t2:int)
(eqs:list _lit) (res:_lit) (clause:C.t) : C.t :=