From d016f69818b30b75d186fb14f440b93b0518fc66 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 21 Nov 2019 15:38:39 +0100 Subject: [coq] Untabify the whole ML codebase. We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ``` --- plugins/btauto/refl_btauto.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/btauto') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 615e9cd140..ec9f9a39e0 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -54,10 +54,10 @@ module Env = struct type t = (int ConstrHashtbl.t * int ref) let add (tbl, off) (t : Constr.t) = - try ConstrHashtbl.find tbl t + try ConstrHashtbl.find tbl t with - | Not_found -> - let i = !off in + | Not_found -> + let i = !off in let () = ConstrHashtbl.add tbl t i in let () = incr off in i @@ -159,7 +159,7 @@ module Btauto = struct | Bool.Xorb (b1, b2) -> lapp f_xor [|convert b1; convert b2|] | Bool.Ifb (b1, b2, b3) -> lapp f_ifb [|convert b1; convert b2; convert b3|] - let convert_env env : Constr.t = + let convert_env env : Constr.t = CoqList.of_list (Lazy.force Bool.typ) env let reify env t = lapp eval [|convert_env env; convert t|] -- cgit v1.2.3