From 1f31ca099259fbea08a7fef56e1989283aec040a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 19 Mar 2008 17:58:43 +0000
Subject: Do another pass on the typeclasses code. Correct globalization of
 class names, gives the ability to specify qualified classes in instance
 declarations. Use that in the class_tactics code. Refine the implementation
 of classes. For singleton classes the implementation of the class becomes a
 regular definition (into Type or Prop). The single method becomes a 'trivial'
 projection that allows to launch typeclass resolution. Each instance is just
 a definition as usual. Examples in theories/Classes/RelationClasses. This
 permits to define [Class reflexive A (R : relation A) := refl : forall x, R x
 x.]. The definition of [reflexive] that is generated is the same as the
 original one. We just need a way to declare arbitrary lemmas as instances of
 a particular class to retrofit existing reflexivity lemmas as typeclass
 instances of the [reflexive] class. Also debug rewriting under binders in
 setoid_rewrite to allow rewriting with lemmas which capture the bound
 variables when applied (works only with setoid_rewrite, as rewrite first
 matches the lemma with the entire, closed term). One can rewrite with [H :
 forall x, R (f x) (g x)] in the goal [exists x, P (f x)].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10697 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/implicit_quantifiers.mli | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'interp/implicit_quantifiers.mli')

diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 4ea95fc43c..9ecdcd6c07 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -20,12 +20,13 @@ open Mod_subst
 open Rawterm
 open Topconstr
 open Util
+open Libnames
 open Typeclasses
 (*i*)
 
 val ids_of_list : identifier list -> Idset.t
-val destClassApp : constr_expr -> identifier located * constr_expr list
-val destClassAppExpl : constr_expr -> identifier located * (constr_expr * explicitation located option) list
+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 ->
@@ -55,10 +56,10 @@ val implicits_of_binders : local_binder list -> (Topconstr.explicitation * (bool
 val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
 
 val combine_params : Names.Idset.t ->
-  (Names.Idset.t -> (Names.identifier * bool) option * (Names.identifier * Term.constr option * Term.types) ->
+  (Names.Idset.t -> (global_reference * bool) option * (Names.identifier * Term.constr option * Term.types) ->
     Topconstr.constr_expr * Names.Idset.t) ->
   (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
-  ((Names.identifier * bool) option * Term.named_declaration) list ->
+  ((global_reference * bool) option * Term.named_declaration) list ->
   Topconstr.constr_expr list * Names.Idset.t
 
 
-- 
cgit v1.2.3