X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=dd915a2829c0831961b860dbc76e02b7805cce8d;hb=08791e80816548121e81e04d3ead8c9a5171d033;hp=9896db7c91ace4970253a72f9db435aff45bea52;hpb=dc690e0dfa17463d516b74d0a7e5aad810ee1b41;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 9896db7c9..dd915a282 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -35,7 +35,7 @@ exception PathNotWellFormed
   (** raised when an environment is not enough informative to decide *)
 exception Try_again
 
-let debug = true
+let debug = false
 let debug_print = if debug then prerr_endline else ignore
 
 (*
@@ -412,14 +412,16 @@ let interpretate_obj ~context ~env ~uri ~is_path obj =
      let field_names = List.map fst fields in
       Cic.InductiveDefinition
        (tyl,[],List.length params,[`Class (`Record field_names)])
-  | TacticAst.Theorem (_,name,ty,bo) ->
+  | TacticAst.Theorem (flavour, name, ty, bo) ->
+     let attrs = [`Flavour flavour] in
      let ty' = interpretate_term [] env None false ty in
-     match bo with
+     (match bo with
         None ->
-         Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],[])
+         Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
       | Some bo ->
          let bo' = Some (interpretate_term [] env None false bo) in
-          Cic.Constant (name,bo',ty',[],[])
+          Cic.Constant (name,bo',ty',[],attrs))
+          
 
   (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
 let rev_uniq =