X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataExtractor.ml;h=f9a26637d968db9c4e7cc3129d7f1223af035e55;hb=de4483296d06aac3df4da10d5401b1f97c4350ab;hp=0ffe5980d183cd7ad8a4d8807c2b3adb5d0a55eb;hpb=71215a7e5b10535b538776680dce5dc02e118c2f;p=helm.git

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index 0ffe5980d..f9a26637d 100644
--- a/helm/ocaml/metadata/metadataExtractor.ml
+++ b/helm/ocaml/metadata/metadataExtractor.ml
@@ -63,8 +63,8 @@ module S = MetadataSet
 let unopt = function Some x -> x | None -> assert false
 
 let incr_depth = function
-  | `MainConclusion (Some depth) -> `MainConclusion (Some (depth + 1))
-  | `MainHypothesis (Some depth) -> `MainHypothesis (Some (depth + 1))
+  | `MainConclusion (Some (Eq depth)) -> `MainConclusion (Some (Eq (depth + 1)))
+  | `MainHypothesis (Some (Eq depth)) -> `MainHypothesis (Some (Eq (depth + 1)))
   | _ -> assert false
 
 let var_has_body uri =
@@ -103,7 +103,7 @@ let compute_term pos term =
     | Cic.Prod (_, source, target) ->
         (match pos with
         | `MainConclusion _ ->
-            let set = aux (`MainHypothesis (Some 0)) set source in
+            let set = aux (`MainHypothesis (Some (Eq 0))) set source in
             aux (incr_depth pos) set target
         | `MainHypothesis _ ->
             let set = aux `InHypothesis set source in
@@ -300,8 +300,8 @@ let rec compute_var pos uri =
           List.flatten 
             (List.map (compute_var (next_pos pos)) params) in 
 	(match pos with
-	   | `MainHypothesis (Some 0) -> 
-	       let pos = `MainHypothesis (Some (depth_offset params)) in
+	   | `MainHypothesis (Some (Eq 0)) -> 
+	       let pos = `MainHypothesis (Some (Eq (depth_offset params))) in
 		 (compute pos ~body:None ~ty)@metadata_of_vars
 	   | `InHypothesis ->
 	        (compute pos ~body:None ~ty)@metadata_of_vars
@@ -313,23 +313,23 @@ let compute_obj uri =
   match o with
   | Cic.Variable (_, body, ty, params, _)
   | Cic.Constant (_, body, ty, params, _) -> 
-      let pos = `MainConclusion (Some (depth_offset params)) in
+      let pos = `MainConclusion (Some (Eq (depth_offset params))) in
       let metadata = compute pos ~body ~ty
       in
       let metadata_of_vars = 
         List.flatten 
-          (List.map (compute_var (`MainHypothesis (Some 0))) params) 
+          (List.map (compute_var (`MainHypothesis (Some (Eq 0)))) params) 
       in
       [UriManager.string_of_uri uri, 
          UriManager.name_of_uri uri,metadata @ metadata_of_vars]
   | Cic.InductiveDefinition (types, params, _, _) ->
-      let pos = `MainConclusion(Some (depth_offset params)) in
+      let pos = `MainConclusion(Some (Eq (depth_offset params))) in
       let metadata_of_vars = 
         List.flatten 
-          (List.map (compute_var (`MainHypothesis (Some 0))) params) in
+          (List.map (compute_var (`MainHypothesis (Some (Eq 0)))) params) in
       let metadata = compute_ind pos ~uri ~types in
 	List.map (fun (uri,name,md) -> (uri,name,md@metadata_of_vars)) metadata
   | Cic.CurrentProof _ -> assert false    
 
 
-let compute ~body ~ty = compute (`MainConclusion (Some 0)) ~body ~ty 
+let compute ~body ~ty = compute (`MainConclusion (Some (Eq 0))) ~body ~ty