Commit 3c5580d0 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

minor : Adding comment

parent 83b74fbd
......@@ -20,6 +20,9 @@ open Ty
open Term
open Decl
(* This label is used to stop the introduction transformation to introduce
variables past it. It is generated by software that uses why3 as a backend
such as SPARK (for counterexamples) *)
let stop_intro = Ident.create_label "stop_intro"
let rec intros pr f =
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