From 208eceab14148fa561c36f71e2e1485e73832616 Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Wed, 4 Nov 2009 18:47:36 +0000
Subject: 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
---
 pretyping/recordops.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'pretyping')

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] *)
-- 
cgit v1.2.3