From 1a09e2340adef947981178e266c0ba4ea6b23869 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 22 Jul 2009 11:15:41 +0000 Subject: [PATCH] leftno was List.length rights :-) --- helm/software/components/ng_tactics/nTactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 16602ac9f..895d7c3f0 100644 --- 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; -- 2.39.2