From bde29698c58eb36166753a30765a92e602e9cc78 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Apr 2007 14:24:30 +0000 Subject: [PATCH] you can case even if only a right appears... so, substituting them for metas is wrong, rels are better --- helm/software/components/tactics/primitiveTactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 5310fea7e..8787b1a73 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -711,7 +711,7 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam let rec mkargs = function | 0 -> [] | 1 -> [Cic.Rel 1] - | n -> (Cic.Implicit None)::(mkargs (n-1)) + | n -> (Cic.Rel n)::(mkargs (n-1)) in mkargs n_lambdas in -- 2.39.2