From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 plugins/cc/ccalgo.mli | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'plugins/cc/ccalgo.mli')

diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 8786c907..78dbee3f 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ccalgo.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Term
 open Names
@@ -24,6 +22,8 @@ type term =
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
 
+val term_equal : term -> term -> bool
+
 type patt_kind =
     Normal
   | Trivial of types
@@ -66,13 +66,16 @@ type explanation =
   | Contradiction of disequality
   | Incomplete
 
+module Constrhash : Hashtbl.S with type key = constr
+module Termhash : Hashtbl.S with type key = term
+
 val constr_of_term : term -> constr
 
 val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit
 
 val forest : state -> forest
 
-val axioms : forest -> (constr, term * term) Hashtbl.t
+val axioms : forest -> (term * term) Constrhash.t
 
 val epsilons : forest -> pa_constructor list
 
@@ -127,7 +130,7 @@ val do_match :  state ->
 
 val init_pb_stack : state -> matching_problem Stack.t
 
-val paf_of_patt : (term, int) Hashtbl.t -> ccpattern -> pa_fun
+val paf_of_patt : int Termhash.t -> ccpattern -> pa_fun
 
 val find_instances : state -> (quant_eq * int array) list
 
-- 
cgit v1.2.3