Merge tag 'upstream/8.5_beta1+dfsg'

Upstream version 8.5~beta1+dfsg

1 files changed, 0 insertions, 47 deletions

diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
deleted file mode 100644
index b15bc922..00000000
--- a/tactics/nbtermdn.mli
+++ /dev/null
@@ -1,47 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Term
-open Pattern
-open Libnames
-
-(** Named, bounded-depth, term-discrimination nets. *)
-module Make :
-  functor (Y:Map.OrderedType) ->
-sig
-  
-  module Term_dn : sig     
-    type term_label = 
-      | GRLabel of global_reference
-      | ProdLabel 
-      | LambdaLabel
-      | SortLabel
-  end 
-    
-  type 'na t
-  type 'na frozen_t
-    
-  val create : unit -> 'na t
-    
-  val add : 'na t -> ('na * (constr_pattern * Y.t)) -> unit
-  val rmv : 'na t -> 'na -> unit
-  val in_dn : 'na t -> 'na -> bool
-  val remap : 'na t -> 'na -> (constr_pattern * Y.t) -> unit
-    
-  val lookup : 'na t -> constr -> (constr_pattern * Y.t) list
-  val app : ('na -> (constr_pattern * Y.t) -> unit) -> 'na t -> unit
-    
-  val dnet_depth : int ref
-    
-
-  val freeze : 'na t -> 'na frozen_t
-  val unfreeze : 'na frozen_t -> 'na t -> unit
-  val empty : 'na t -> unit
-  val to2lists : 'na t -> ('na * (constr_pattern * Y.t)) list * 
-    (Term_dn.term_label option * Btermdn.Make(Y).t) list
-end