Commit 501d4023 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make realization checking less sensible to whitespace issues.

parent 24d6caf1
......@@ -24,7 +24,7 @@ cp -r lib/coq $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make GENERATED_PREFIX_COQ="$TMPREAL/lib/coq" update-coq > /dev/null 2> /dev/null
LANG=C diff -r -q -x '*.bak' -x '*~' -x '*.aux' lib/coq $TMPREAL/lib/coq > $TMPREAL/diff-coq
LANG=C diff -w -r -q -x '*.bak' -x '*~' -x '*.aux' lib/coq $TMPREAL/lib/coq > $TMPREAL/diff-coq
if test -s "$TMPREAL/diff-coq"; then
echo "Coq realizations FAILED, please regenerate and prove them"
sed -e "s,$TMPREAL/lib/coq,new," $TMPREAL/diff-coq
......
......@@ -18,5 +18,6 @@ Require map.Map.
(* Why3 assumption *)
Definition const {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}
(v:b): (a -> b) := fun (us:a) => v.
(v:b) : a -> b :=
fun (us:a) => v.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment