From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 toplevel/autoinstance.mli | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 toplevel/autoinstance.mli

(limited to 'toplevel/autoinstance.mli')

diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli
new file mode 100644
index 00000000..3866fff3
--- /dev/null
+++ b/toplevel/autoinstance.mli
@@ -0,0 +1,38 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+(*i*)
+open Term
+open Libnames
+open Typeclasses
+open Names
+open Evd
+open Sign
+(*i*)
+
+(*s Automatic detection of (some) record instances *)
+
+(* What to do if we find an instance. Passed are : the reference
+ * representing the record/class (definition or constructor) *)
+type instance_decl_function = global_reference -> rel_context -> constr list -> unit
+
+(* [search_declaration gr] Search in the library if the (new)
+ * declaration gr can form an instance of a registered record/class *)
+val search_declaration : global_reference -> unit
+
+(* [search_record declf gr evm] Search the library for instances of
+   the (new) record/class declaration [gr], and register them using
+   [declf]. [evm] is the signature of the record (to avoid recomputing
+   it) *)
+val search_record : instance_decl_function -> global_reference -> evar_map -> unit
+
+(* Instance declaration for both scenarios *)
+val declare_record_instance : instance_decl_function
+val declare_class_instance : instance_decl_function
-- 
cgit v1.2.3