diff options
| -rwxr-xr-x | pretyping/recordops.ml | 1 | ||||
| -rwxr-xr-x | pretyping/recordops.mli | 4 |
2 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index ef0e839bb..d02ca06db 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -43,6 +43,7 @@ let (inStruc,outStruc) = let add_new_struc (s,c,n,l) = Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l})) +let find_structure indsp = List.assoc indsp !sTRUCS (*** table des definitions "object" : pour chaque object c, c := [x1:B1]...[xk:Bk](R_Cons a1...am t1...t_n) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 7d28eeffb..f82e074ba 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -24,6 +24,10 @@ type struc_typ = { val add_new_struc : inductive_path * identifier * int * section_path option list -> unit +(* [find_structure isp] returns the infos associated to inductive path + [isp] if it corresponds to a structure, otherwise fails with [Not_found] *) +val find_structure : inductive_path -> struc_typ + type obj_typ = { o_DEF : constr; o_TABS : constr list; (* dans l'ordre *) |