From c3ca134628ad4d9ef70a13b65c48ff17c737238f Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 18 Dec 2012 18:52:54 +0000
Subject: Modulification of name

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml         | 2 +-
 proofs/logic.mli        | 2 +-
 proofs/tactic_debug.mli | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index ba85be766a..c48882c1a1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -26,7 +26,7 @@ type refiner_error =
 
   (* Errors raised by the refiner *)
   | BadType of constr * constr * constr
-  | UnresolvedBindings of name list
+  | UnresolvedBindings of Name.t list
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
diff --git a/proofs/logic.mli b/proofs/logic.mli
index e87adb1654..40feb5c56f 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -39,7 +39,7 @@ type refiner_error =
 
   (*i Errors raised by the refiner i*)
   | BadType of constr * constr * constr
-  | UnresolvedBindings of name list
+  | UnresolvedBindings of Name.t list
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 2ba1b315b9..8afee3418d 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -46,7 +46,7 @@ val db_pattern_rule :
 
 (** Prints a matched hypothesis *)
 val db_matched_hyp :
-  debug_info -> env -> Id.t * constr option * constr -> name -> unit
+  debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit
 
 (** Prints the matched conclusion *)
 val db_matched_concl : debug_info -> env -> constr -> unit
@@ -56,7 +56,7 @@ val db_mc_pattern_success : debug_info -> unit
 
 (** Prints a failure message for an hypothesis pattern *)
 val db_hyp_pattern_failure :
-  debug_info -> env -> name * constr_pattern match_pattern -> unit
+  debug_info -> env -> Name.t * constr_pattern match_pattern -> unit
 
 (** Prints a matching failure message for a rule *)
 val db_matching_failure : debug_info -> unit
-- 
cgit v1.2.3