From: Stefano Zacchiroli 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