From bd55e2b2787bbabf7fba126126611c58548424fc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 16 Jun 2016 18:49:07 +0200
Subject: Shrink Proofs/Obligations by default and deprecate

Fix bug in Shrink obligations with Program in the process.

Fix implementation of shrink for abstract proofs

- Update doc in term.mli to reflect the fact that let-in's
  are part of what is returned by [decompose_lam_assum].
---
 tactics/tactics.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e264505314..f3e117f8c3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -119,12 +119,12 @@ let _ =
 
 (* Shrinking of abstract proofs. *)
 
-let shrink_abstract = ref false
+let shrink_abstract = ref true
 
 let _ =
   declare_bool_option
     { optsync  = true;
-      optdepr  = false;
+      optdepr  = true;
       optname  = "shrinking of abstracted proofs";
       optkey   = ["Shrink"; "Abstract"];
       optread  = (fun () -> !shrink_abstract) ;
@@ -4774,7 +4774,7 @@ let rec shrink ctx sign c t accu =
   match ctx, sign with
   | [], [] -> (c, t, accu)
   | p :: ctx, decl :: sign ->
-      if noccurn 1 c then
+      if noccurn 1 c && noccurn 1 t then
         let c = subst1 mkProp c in
         let t = subst1 mkProp t in
         shrink ctx sign c t accu
-- 
cgit v1.2.3