diff options
| author | gmelquio | 2009-11-04 18:47:36 +0000 |
|---|---|---|
| committer | gmelquio | 2009-11-04 18:47:36 +0000 |
| commit | 208eceab14148fa561c36f71e2e1485e73832616 (patch) | |
| tree | 3763b73a349cca213cee543f8cf0204d65594ae6 /pretyping | |
| parent | fc7f18e8596a8b4e690ff726edb02a7cf319edbd (diff) | |
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
Fixed pretty printing of record syntax.
Allowed record syntax inside patterns. (Patch by Cedric Auger.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rwxr-xr-x | pretyping/recordops.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 5d3180ff7b..0af25666d4 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -30,6 +30,11 @@ type struc_typ = { val declare_structure : inductive * constructor * (name * bool) list * constant option list -> unit +(* [lookup_structure isp] returns the struc_typ associated to the + inductive path [isp] if it corresponds to a structure, otherwise + it fails with [Not_found] *) +val lookup_structure : inductive -> struc_typ + (* [lookup_projections isp] returns the projections associated to the inductive path [isp] if it corresponds to a structure, otherwise it fails with [Not_found] *) |