From 60c5983bf954e362307e3db679bad1c32096ff6d 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 --- components/tactics/primitiveTactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 5310fea7e..8787b1a73 100644 --- a/components/tactics/primitiveTactics.ml +++ b/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