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 --- interp/topconstr.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'interp/topconstr.mli') diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 0064d238d..b6e2927bb 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -33,6 +33,7 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr + | ARecord of aconstr option * (identifier * aconstr) list | ACases of case_style * aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * (cases_pattern list * aconstr) list @@ -133,6 +134,7 @@ type constr_expr = | CAppExpl of loc * (proj_flag * reference) * constr_expr list | CApp of loc * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list + | CRecord of loc * constr_expr option * (identifier located * constr_expr) list | CCases of loc * case_style * constr_expr option * (constr_expr * (name option * constr_expr option)) list * (loc * cases_pattern_expr list located list * constr_expr) list -- cgit v1.2.3