From d8e0b34863a7359fb54fdbf9d747d7b624713130 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 17 Apr 2007 08:41:09 +0000 Subject: [PATCH] fixed a list.nth called on a too short list --- helm/software/components/tactics/proofEngineReduction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml index ec6907436..016a7ba99 100644 --- a/helm/software/components/tactics/proofEngineReduction.ml +++ b/helm/software/components/tactics/proofEngineReduction.ml @@ -1023,7 +1023,7 @@ let simpl context = prerr_endline ("e piglio il rispettivo in :"^String.concat " " (List.map (fun x -> CicPp.ppterm x) original_args)); (* look for args[regno] in saved_args *) - let wanted = List.nth args (guess_recno uri) in (* args@l ? *) + let wanted = List.nth (args@l) (guess_recno uri) in let rec aux n = function | [] -> n (* DA CAPIRE *) | t::_ when t = wanted -> n -- 2.39.2