X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicParser.ml;h=3d1d3d1aa05ccbcd1ee313d8574b870b09fad3bd;hb=cc23f034c9419186602d9250456241f2eba90d7c;hp=8334ccfb62e65aac3e4162731b23d2b3078b5597;hpb=94538d45a28cf8e833f9ad4523b61a3252fde7d4;p=helm.git

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 8334ccfb6..3d1d3d1aa 100644
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -60,7 +60,7 @@ type stack_entry =
       (* id, name, type, body *)
   | Constructor of string * Cic.annterm   (* name, type *)
   | Decl of Cic.id * Cic.name * Cic.annterm (* id, binder, source *)
-  | Def of Cic.id * Cic.name * Cic.annterm  (* id, binder, source *)
+  | Def of Cic.id * Cic.name * Cic.annterm * Cic.annterm  (* id, binder, source, type *)
   | Fix_fun of Cic.id * string * int * Cic.annterm * Cic.annterm
       (* id, name, ind. index, type, body *)
   | Inductive_type of string * string * bool * Cic.annterm *
@@ -97,7 +97,7 @@ let string_of_stack ctxt =
       | Constructor (name, _) -> "Constructor " ^ name
       | Cofix_fun (id, _, _, _) -> sprintf "Cofix_fun (id=%s)" id
       | Decl (id, _, _) -> sprintf "Decl (id=%s)" id
-      | Def (id, _, _) -> sprintf "Def (id=%s)" id
+      | Def (id, _, _, _) -> sprintf "Def (id=%s)" id
       | Fix_fun (id, _, _, _, _) -> sprintf "Fix_fun (id=%s)" id
       | Inductive_type (id, name, _, _, _) ->
           sprintf "Inductive_type %s (id=%s)" name id
@@ -406,14 +406,15 @@ let end_element ctxt tag =
         | ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
         | _ -> attribute_error ())
   | "def" ->  (* same as "decl" above *)
+      let ty = pop_cic ctxt in
       let source = pop_cic ctxt in
       push ctxt
         (match pop_tag_attrs ctxt with
         | ["binder", binder; "id", id]
         | ["binder", binder; "id", id; "sort", _] ->
-            Def (id, Cic.Name binder, source)
+            Def (id, Cic.Name binder, source, ty)
         | ["id", id]
-        | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source)
+        | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source, ty)
         | _ -> attribute_error ())
   | "arity"           (* transparent elements (i.e. which contain a CIC) *)
   | "body"
@@ -467,8 +468,8 @@ let end_element ctxt tag =
   | "LETIN" ->
       let target = pop_cic ctxt in
       let rec add_def target = function
-        | Def (id, binder, source) :: tl ->
-            add_def (Cic.ALetIn (id, binder, source, target)) tl
+        | Def (id, binder, source, ty) :: tl ->
+            add_def (Cic.ALetIn (id, binder, source, ty, target)) tl
         | tl ->
             ctxt.stack <- tl;
             target