From 5cabee90acd79a46519b2051ff8ac83d8ec35321 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Nov 2007 10:10:33 +0000
Subject: [PATCH] Type application and abstractions are now exported correctly.

---
 .../cic_exportation/cicExportation.ml           | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index 769dc916c..94cd982fe 100644
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -164,8 +164,10 @@ let rec pp t context =
     | C.Implicit _ -> "?"
     | C.Prod (b,s,t) ->
        (match b with
-          C.Name n -> "(\\forall " ^ n ^ ":" ^ pp s context ^ "." ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")"
-        | C.Anonymous -> "(" ^ pp s context ^ "\\to " ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")"
+          C.Name n ->
+           let n = "'" ^ String.uncapitalize n in
+            "(" ^ pp s context ^ " -> " ^ pp t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
+        | C.Anonymous -> "(" ^ pp s context ^ " -> " ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")"
        )
     | C.Cast (v,t) -> pp v context
     | C.Lambda (b,s,t) ->
@@ -176,6 +178,10 @@ let rec pp t context =
     | C.LetIn (b,s,t) ->
        let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph in
        "(let " ^ ppname b ^ " = " ^ pp s context ^ " in " ^ pp t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")"
+    | C.Appl (C.MutInd _ as he::tl) ->
+       let hes = pp he context in
+       let stl = String.concat "," (clean_args_for_ty context tl) in
+        (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
     | C.Appl (C.MutConstruct _ as he::tl) ->
        let hes = pp he context in
        let stl = String.concat "," (clean_args context tl) in
@@ -338,6 +344,13 @@ and clean_args context =
        `Type -> None
      | `Proof -> None
      | `Term -> Some pp t context)
+and clean_args_for_ty context =
+ HExtlib.filter_map
+  (function t ->
+    match analyze_term context t with
+       `Type -> Some pp t context
+     | `Proof -> None
+     | `Term -> None)
 in
  pp
 ;;
-- 
2.39.2