X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Fprocedural1.ml;h=4b91270028139a7a57b4c026c0bfef011d09eb69;hb=cb75149567a9a21206760211eeefcd5f26321bcb;hp=b3e11285049dde07d36b3c1b064f90dca9934a38;hpb=df3e9efe1690fb5d93061b657e6ddcc3c11745db;p=helm.git

diff --git a/helm/software/components/acic_procedural/procedural1.ml b/helm/software/components/acic_procedural/procedural1.ml
index b3e112850..4b9127002 100644
--- a/helm/software/components/acic_procedural/procedural1.ml
+++ b/helm/software/components/acic_procedural/procedural1.ml
@@ -45,7 +45,6 @@ module Cl   = ProceduralClassify
 module T    = ProceduralTypes
 module Cn   = ProceduralConversion
 module H    = ProceduralHelpers
-module X    = ProceduralTeX
 
 type status = {
    sorts : (C.id, A.sort_kind) Hashtbl.t;
@@ -140,14 +139,16 @@ try
       | {A.annsynthesized = st; A.annexpected = None}    -> Some (st, st)
    with Not_found -> None
 with Invalid_argument _ -> failwith "A2P.get_inner_types"
-(*
-let get_inner_sort st v =
+
+let is_proof st v =
 try
    let id = Ut.id_of_annterm v in
-   try Hashtbl.find st.sorts id
-   with Not_found -> `Type (CicUniv.fresh())
-with Invalid_argument _ -> failwith "A2P.get_sort"
-*)
+   try match Hashtbl.find st.sorts id with
+      | `Prop -> true
+      | _     -> false
+   with Not_found -> H.is_proof st.context (H.cic v)
+with Invalid_argument _ -> failwith "P1.is_proof"
+
 let get_entry st id =
    let rec aux = function
       | []                                        -> assert false
@@ -472,9 +473,10 @@ let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
 
 let def_flavours = [`Definition]
 
-let get_flavour ?flavour attrs =
+let get_flavour ?flavour st v attrs =
    let rec aux = function
-      | []               -> List.hd th_flavours
+      | []               -> 
+         if is_proof st v then List.hd th_flavours else List.hd def_flavours
       | `Flavour fl :: _ -> fl
       | _ :: tl          -> aux tl
    in
@@ -484,7 +486,7 @@ let get_flavour ?flavour attrs =
 
 let proc_obj ?flavour ?(info="") st = function
    | C.AConstant (_, _, s, Some v, t, [], attrs)         ->
-      begin match get_flavour ?flavour attrs with
+      begin match get_flavour ?flavour st v attrs with
          | flavour when List.mem flavour th_flavours  ->
             let ast = proc_proof st v in
             let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in