From 07713b63c109a99c2b9dc7265571bcdd3dd6ed0d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Sep 2009 11:41:21 +0000
Subject: [PATCH] let rec/corec and co/inductive are not printed!

---
 .../components/content_pres/content2pres.ml   | 14 ++++++----
 .../ng_cic_content/nTermCicContent.ml         | 26 +++++++++++++++++--
 2 files changed, 33 insertions(+), 7 deletions(-)

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 63eec5e35..9c389467c 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -927,17 +927,20 @@ let inductive2pres term2pres ind =
 
 let definition2pres ?recno term2pres d =
   let name = match d.Content.def_name with Some x -> x|_->assert false in
-  let rno = match recno with None -> assert false | Some x -> x in
+  let rno = match recno with None -> -1 (* cofix *) | Some x -> x in
   let ty = d.Content.def_type in
   let module P = CicNotationPt in
   let rec split_pi i t = 
     if i <= 1 then 
       match t with 
-      | P.Binder ((`Pi|`Forall),(var,_ as v),t) -> [v], var, t 
+      | P.Binder ((`Pi|`Forall),(var,_ as v),t) 
+      | P.AttributedTerm (_,P.Binder ((`Pi|`Forall),(var,_ as v),t)) -> 
+            [v], var, t 
       | _ -> assert false
     else
       match t with
-      | P.Binder ((`Pi|`Forall), var ,ty) ->
+      | P.Binder ((`Pi|`Forall), var ,ty) 
+      | P.AttributedTerm (_, P.Binder ((`Pi|`Forall), var ,ty)) ->
            let l, r, t = split_pi (i-1) ty in
            var :: l, r, t
       | _ -> assert false
@@ -955,8 +958,9 @@ let definition2pres ?recno term2pres d =
   in
   B.b_hv [] 
    [B.b_hv [] 
-    ([ B.b_space; B.b_text [] name ] @ params @
-       [B.b_kw "on" ; B.b_space; term2pres rec_param ; B.b_space;
+    ([ B.b_space; B.b_text [] name; B.b_space ] @ params @
+    (if rno <> -1 then [B.b_kw "on" ; B.b_space; term2pres rec_param ] else [])
+    @[ B.b_space;
        B.b_text [] ":"; B.b_space; term2pres ty]); 
    B.b_text [] ":=";
    B.b_h [] [B.b_space;term2pres body] ]
diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml
index 56a3f3507..3c17823b6 100644
--- a/helm/software/components/ng_cic_content/nTermCicContent.ml
+++ b/helm/software/components/ng_cic_content/nTermCicContent.ml
@@ -559,15 +559,37 @@ let build_inductive b seed =
             K.inductive_type = ty;
             K.inductive_constructors = build_constructors seed cl
            }
+in
+let build_fixpoint b seed = 
+      fun (_,n,_,ty,t) ->
+        let t = nast_of_cic ~context:[] t in
+        let ty = nast_of_cic ~context:[] ty in
+        `Definition
+          { K.def_id = gen_id inductive_prefix seed;
+            K.def_name = Some n;
+            K.def_aref = "";
+            K.def_type = ty;
+            K.def_term = t;
+           }
 in
   let res =
    match kind with
-    | NCic.Fixpoint (is_rec, ifl, _) -> assert false
+    | NCic.Fixpoint (is_rec, ifl, _) -> 
+         (gen_id object_prefix seed, [], conjectures,
+            `Joint
+              { K.joint_id = gen_id joint_prefix seed;
+                K.joint_kind = 
+                   if is_rec then 
+                        `Recursive (List.map (fun (_,_,i,_,_) -> i) ifl)
+                   else `CoRecursive;
+                K.joint_defs = List.map (build_fixpoint is_rec seed) ifl
+              }) 
     | NCic.Inductive (is_ind, lno, itl, _) ->
          (gen_id object_prefix seed, [], conjectures,
             `Joint
               { K.joint_id = gen_id joint_prefix seed;
-                K.joint_kind = `Inductive lno;
+                K.joint_kind = 
+                   if is_ind then `Inductive lno else `CoInductive lno;
                 K.joint_defs = List.map (build_inductive is_ind seed) itl
               }) 
     | NCic.Constant (_,_,Some bo,ty,_) ->
-- 
2.39.2