https://github.com/EasyCrypt/easycrypt
Revision 89618ebb9290a5dbec3fe1a6a57b441bcba18a63 authored by Pierre-Yves Strub on 15 November 2017, 06:54:48 UTC, committed by Pierre-Yves Strub on 15 November 2017, 06:54:48 UTC
Syntax is: wlog: x1 ... xn / form. It transforms the goal G into: |- (forall x1 ... xn, form => G) => G |- form => G
1 parent 1923b91
Tip revision: 89618ebb9290a5dbec3fe1a6a57b441bcba18a63 authored by Pierre-Yves Strub on 15 November 2017, 06:54:48 UTC
New tactic: wlog (without loss of generality).
New tactic: wlog (without loss of generality).
Tip revision: 89618eb
ecPException.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2017 - Inria
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
type exn_printer = Format.formatter -> exn -> unit
(* -------------------------------------------------------------------- *)
let exn_printers = (Stack.create () : exn_printer Stack.t)
(* -------------------------------------------------------------------- *)
let core_printer fmt exn =
Format.fprintf fmt "anomaly: %s, please report to: @\n@." (Printexc.to_string exn);
Format.fprintf fmt "anomaly: \t%s@\n@." EcVersion.url
(* -------------------------------------------------------------------- *)
let () = Stack.push core_printer exn_printers
(* -------------------------------------------------------------------- *)
let register ppexn = Stack.push ppexn exn_printers
let () = register Why3.Exn_printer.exn_printer
(* -------------------------------------------------------------------- *)
exception Exit_loop
let exn_printer fmt exn =
let do1 (f : exn_printer) =
try
Format.fprintf fmt "@[%a@]@." f exn;
raise Exit_loop
with e when e <> Exit_loop -> ()
in
try Stack.iter do1 exn_printers
with Exit_loop -> ()
(* -------------------------------------------------------------------- *)
let tostring (e : exn) =
let buf = Buffer.create 128 in
let fmt = Format.formatter_of_buffer buf in
exn_printer fmt e; Buffer.contents buf
Computing file changes ...