leftno was List.length rights :-)

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 16602ac9f6202276e623c7e206df3289c03c79a9..895d7c3f0666007e61a4b78f6c9d2b728d60eaa4 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -450,7 +450,7 @@ let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
   let status, what = disambiguate status what None (ctx_of goalty) in
   let status, ty_what = typeof status (ctx_of what) what in 
   let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
-  let leftno = List.length rights in
+  let leftno = List.length lefts in
   let rightno = List.length rights in
   indtyref := Some { 
     rightno = rightno; leftno = leftno; consno = consno;