From 04ae8084273d40d58a391a5a530511c975fbd22d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 25 Aug 2009 11:32:17 +0000 Subject: [PATCH] ncoindutive now generates a co-inductive type, not an inductive one --- .../components/ng_disambiguation/nCicDisambiguate.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 357f9e539..ae6284cc8 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -509,13 +509,11 @@ let interpretate_obj let add_params = List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in let leftno = List.length params in + let _,inductive,_,_ = try List.hd tyl with Failure _ -> assert false in let obj_context = snd ( List.fold_left (fun (i,res) (name,_,_,_) -> - let _,inductive,_,_ = - (* ??? *) - try List.hd tyl with Failure _ -> assert false in let nref = NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno)) in @@ -545,7 +543,7 @@ let interpretate_obj let height = (* XXX calculate *) 0 in let attrs = `Provided, `Regular in uri, height, [], [], - NCic.Inductive (true,leftno,tyl,attrs) + NCic.Inductive (inductive,leftno,tyl,attrs) | CicNotationPt.Record (params,name,ty,fields) -> let context,params = let context,res = -- 2.39.2