]> matita.cs.unibo.it Git - helm.git/commitdiff
ncoindutive now generates a co-inductive type, not an inductive one
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 25 Aug 2009 11:32:17 +0000 (11:32 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 25 Aug 2009 11:32:17 +0000 (11:32 +0000)
helm/software/components/ng_disambiguation/nCicDisambiguate.ml

index 357f9e53977aa10be34f8df4b805304d5cd92041..ae6284cc8a6eb01a2ee47bb172c3617a025e73bd 100644 (file)
@@ -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 =