fixed instance

[helm.git] / helm / ocaml / metadata / metadataExtractor.ml

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index 0ffe5980d183cd7ad8a4d8807c2b3adb5d0a55eb..f9a26637d968db9c4e7cc3129d7f1223af035e55 100644 (file)
--- 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