added attributes support

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index b7dda108592449434fccc60d601b572acf49e806..7845818b716777b6109287569541439240c04d40 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -214,7 +214,7 @@ module Cache :
              C.CoFix (i, liftedfl)
       in
       function
-         C.Constant (name,bo,ty,params) ->
+         C.Constant (name,bo,ty,params,attrs) ->
            let bo' =
              match bo with
                None -> None
@@ -222,8 +222,8 @@ module Cache :
            in
            let ty' = restore_in_term ty in
            let params' = List.map recons params in
-           C.Constant (name, bo', ty', params')
-       | C.CurrentProof (name,conjs,bo,ty,params) ->
+           C.Constant (name, bo', ty', params',attrs)
+       | C.CurrentProof (name,conjs,bo,ty,params,attrs) ->
            let conjs' =
              List.map
                (function (i,hyps,ty) ->
@@ -245,8 +245,8 @@ module Cache :
            let bo' = restore_in_term bo in
            let ty' = restore_in_term ty in
            let params' = List.map recons params in
-           C.CurrentProof (name, conjs', bo', ty', params')
-       | C.Variable (name,bo,ty,params) ->
+           C.CurrentProof (name, conjs', bo', ty', params',attrs)
+       | C.Variable (name,bo,ty,params,attrs) ->
            let bo' =
              match bo with
                None -> None
@@ -254,8 +254,8 @@ module Cache :
            in
            let ty' = restore_in_term ty in
            let params' = List.map recons params in
-           C.Variable (name, bo', ty', params')
-       | C.InductiveDefinition (tl,params,paramsno) ->
+           C.Variable (name, bo', ty', params',attrs)
+       | C.InductiveDefinition (tl,params,paramsno,attrs) ->
            let params' = List.map recons params in
            let tl' =
              List.map (function (name, inductive, ty, constructors) ->
@@ -267,7 +267,7 @@ module Cache :
                  constructors))
                tl
            in
-           C.InductiveDefinition (tl', params', paramsno)
+           C.InductiveDefinition (tl', params', paramsno, attrs)
     ;;
 
     let empty () = 
@@ -668,7 +668,7 @@ let in_cache uri =
 
 let add_type_checked_term uri (obj,ugraph) =
   match obj with 
-      Cic.Constant (s,(Some bo),ty,ul) ->
+      Cic.Constant (s,(Some bo),ty,ul,_) ->
        Cache.add_cooked ~key:uri (obj,ugraph)
     | _ -> 
        assert false