From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 25 Aug 2009 11:32:17 +0000 (+0000)
Subject: ncoindutive now generates a co-inductive type, not an inductive one
X-Git-Tag: make_still_working~3521
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04ae8084273d40d58a391a5a530511c975fbd22d;p=helm.git

ncoindutive now generates a co-inductive type, not an inductive one
---

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 =