From ea0ab5423135a87d1c74d89aad1b2a14d36526d9 Mon Sep 17 00:00:00 2001
From: Martin Clochard <martin.clochard@lri.fr>
Date: Fri, 11 Dec 2015 15:47:56 +0100
Subject: [PATCH] byso: introduce_premises stop at by
---
src/transform/introduction.ml | 3 +++
1 file changed, 3 insertions(+)
diff --git a/src/transform/introduction.ml b/src/transform/introduction.ml
index a899d3034e..60fcf0735d 100644
--- a/src/transform/introduction.ml
+++ b/src/transform/introduction.ml
@@ -21,6 +21,9 @@ open Term
open Decl
let rec intros pr f = match f.t_node with
+ | Tbinop (Timplies,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) },f1)
+ when Slab.mem Term.asym_label f2.t_label ->
+ [create_prop_decl Pgoal pr f]
| Tbinop (Timplies,f1,f2) ->
(* split f1 *)
(* f is going to be removed, preserve its labels and location in f2 *)
--
GitLab