minimal sequent height set to 1

[helm.git] / helm / software / components / ng_tactics / nnAuto.ml

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 0d8655f541d3be63752ea9cf9b414968ae3dea9c..e6010808be96e90216eb511e0b4df0c256bff585 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -1448,7 +1448,7 @@ let fast_height_of_term t =
 let height_of_goals status = 
   let open_goals = head_goals status#stack in
   assert (List.length open_goals > 0);
-  let h = ref 0 in
+  let h = ref 1 in
   List.iter 
     (fun open_goal ->
       let ty = get_goalty status open_goal in