From 0b840f7aaece0c209850adb2a81904b54f410091 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 23 Oct 2008 16:22:18 +0000
Subject: Open notation for declaring record instances. It solves feature
 request 1852, makes me and Arnaud happy and will permit to factor some more
 code in typeclasses. - Records are introduced using the syntax "{| x := t; y
 := foo |}" and "with" clauses are currently parsed but not yet supported in
 the elaboration. You are invited to suggest other syntaxes :) - Missing
 fields are turned into holes, extra fields cause an error message. The
 current implementation finds the type of the record at pretyping time, from
 the typing constraint alone (and just expects an inductive with one
 constructor). It is then impossible to use scope information to parse the
 bodies: that may be wrong. The other solution I see is using the fields to
 detect the type earlier, before internalisation of the bodies, but then we
 get in name clash hell. - In funind/contrib/interface I mostly put [assert
 false] everywhere to avoid warnings.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11496 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/depends.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'contrib/interface')

diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 203bc9e3dd..e7c6c5bcbf 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -210,6 +210,8 @@ let rec depends_of_rawconstr rc acc = match rc with
   | RLambda (_, _, _, rct, rcb)
   | RProd   (_, _, _, rct, rcb)
   | RLetIn  (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc)
+  | RRecord (_, w, l) -> depends_of_rawconstr_list (List.map snd l)
+      (Option.fold_right depends_of_rawconstr w acc)
   | RCases  (_, _, rco, tmt, cc) ->
       (* LEM TODO: handle the cc *)
       (Option.fold_right depends_of_rawconstr rco
-- 
cgit v1.2.3