From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 proofs/logic.mli | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

(limited to 'proofs/logic.mli')

diff --git a/proofs/logic.mli b/proofs/logic.mli
index 1044b59e..d034b73c 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,9 +8,7 @@
 
 open Names
 open Term
-open Sign
 open Evd
-open Environ
 open Proof_type
 
 (** This suppresses check done in [prim_refiner] for the tactic given in
@@ -32,10 +30,6 @@ val with_check    : tactic -> tactic
 
 val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
 
-type proof_variable
-
-
-val proof_variable_index : identifier -> proof_variable list -> int
 
 (** {6 Refiner errors. } *)
 
@@ -43,7 +37,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
@@ -51,8 +45,12 @@ type refiner_error =
 
   (*i Errors raised by the tactics i*)
   | IntroNeedsProduct
-  | DoesNotOccurIn of constr * identifier
+  | DoesNotOccurIn of constr * Id.t
+  | NoSuchHyp of Id.t
 
 exception RefinerError of refiner_error
 
 val catchable_exception : exn -> bool
+
+val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
+  Context.named_declaration -> Environ.named_context_val
-- 
cgit v1.2.3