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/implicit_quantifiers.mli | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'interp/implicit_quantifiers.mli')

diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 5934272091..dc83e2135c 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -28,19 +28,20 @@ val ids_of_list : identifier list -> Idset.t
 val destClassApp : constr_expr -> loc * reference * constr_expr list
 val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list
 
-val free_vars_of_constr_expr :     Topconstr.constr_expr ->
-    ?bound:Idset.t ->
-  Names.identifier list -> Names.identifier list
+(* Fragile, should be used only for construction a set of identifiers to avoid *)
 
-val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list
-
-val binder_list_of_ids : identifier list -> local_binder list
-
-val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
+  identifier list -> identifier list
 
 val free_vars_of_binders :
   ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
 
+(* Returns the free ids in left-to-right order with the location of their first occurence *)
+
+val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list
+
+val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+
 val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
 
 val combine_params_freevar :
-- 
cgit v1.2.3