From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 21 Jan 2005 09:21:35 +0000 (+0000)
Subject: added attributes support
X-Git-Tag: V_0_1_0~109
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9c960d672031bc9ffabb6467bcb13a9e1c55495c;p=helm.git

added attributes support
---

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index b7dda1085..7845818b7 100644
--- 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