From 65792c85896dab2d3c69e7eafd8ff5c628260773 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 17 Jul 2009 13:39:19 +0000 Subject: [PATCH] Bug fixed: singleton application. --- helm/software/components/ng_tactics/nCicElim.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index 350144f9e..0c1a98ec3 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -107,7 +107,7 @@ let mk_elim uri leftno [it] (outsort,suffix) = let cargs,recursive_args = List.split cargs_and_recursive_args in let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs), - CicNotationPt.Appl (name_of_k name :: cargs @ recursive_args) + mk_appl (name_of_k name :: cargs @ recursive_args) ) cl in let bo = CicNotationPt.Case (rec_arg,None,None,branches) in -- 2.39.2