X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=6848338c3bf06b5c09659bacf069df8deb1385ed;hb=c27b932e5adcf89dc9de0e28f65e3370fe3e6b05;hp=62382c8975d328fae6b22ed6574851918008e584;hpb=f4ef7eec626e7a6fb70cdb71bd2ddb983613ab9f;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 62382c897..6848338c3 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -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 =
@@ -559,7 +561,12 @@ let domain_of_obj ~context ast =
            List.flatten (
             List.rev_map
              (fun (_,ty) -> domain_rev_of_term [] ty) cl) @
-            domain_rev_of_term [] ty) tyl)
+            domain_rev_of_term [] ty) tyl) in
+      let dom = 
+       List.fold_left
+        (fun dom (_,ty) ->
+          domain_rev_of_term [] ty @ dom
+        ) dom params
       in
        List.filter
         (fun name ->
@@ -570,14 +577,17 @@ let domain_of_obj ~context ast =
       let dom =
        List.flatten
         (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
-      let dom' =
+      let dom =
        List.filter
         (fun name->
           not (  List.exists (fun (name',_) -> name = Id name') params
               || List.exists (fun (name',_) -> name = Id name') fields)
         ) dom
       in
-       dom' @ domain_rev_of_term [] ty
+       List.fold_left
+        (fun dom (_,ty) ->
+          domain_rev_of_term [] ty @ dom
+        ) (dom @ domain_rev_of_term [] ty) params
  in
   rev_uniq domain_rev