diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-19 15:44:47 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-19 15:44:47 +0000 |
| commit | deadd9eb4dd81b193ab93c571a6b39b6843c5687 (patch) | |
| tree | 3ab4059ec3c947a77851b3fca87c8365ce4f8c2c /pretyping | |
| parent | 94236aaad5f951ff5d47d9c1f63250081da4607a (diff) | |
Export fonction testant si un inductive est un record
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1154 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -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 *) |