From 84a2a8323e96dc66f03ed856f5f49728853c0b72 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Sep 2009 09:53:19 +0000 Subject: [PATCH] do not fail if the inductive type is mutual, just do not generate the eliminator --- helm/software/components/ng_tactics/nCicElim.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index 79a22b077..9db98de49 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -41,7 +41,7 @@ let mk_appl = | l -> CicNotationPt.Appl l ;; -let mk_elim uri leftno [it] (outsort,suffix) = +let mk_elim uri leftno it (outsort,suffix) = let _,ind_name,ty,cl = it in let srec_name = ind_name ^ "_" ^ suffix in let rec_name = mk_id srec_name in @@ -170,7 +170,7 @@ let ast_of_sort s = let mk_elims (uri,_,_,_,obj) = match obj with - NCic.Inductive (true,leftno,itl,_) -> + NCic.Inductive (true,leftno,[itl],_) -> List.map (fun s -> mk_elim uri leftno itl (ast_of_sort s)) (NCic.Prop:: List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ())) -- 2.39.2