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 ``` --- pretyping/program.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/program.ml') diff --git a/pretyping/program.ml b/pretyping/program.ml index a15e66f329..1bc31646dd 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -11,7 +11,7 @@ open CErrors open Util -let papp evdref r args = +let papp evdref r args = let open EConstr in let gr = delayed_force r in let evd, hd = Evarutil.new_global !evdref gr in -- cgit v1.2.3