From f2efd4d7dc9907a569a352bdc5fb8409d9f18360 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 5 Apr 2006 13:24:35 +0000 Subject: [PATCH] a bit of shareing --- components/cic/discrimination_tree.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/components/cic/discrimination_tree.ml b/components/cic/discrimination_tree.ml index bab98921d..18bc73eb5 100644 --- a/components/cic/discrimination_tree.ml +++ b/components/cic/discrimination_tree.ml @@ -37,9 +37,10 @@ module DiscriminationTreeIndexing = let arities = Hashtbl.create 11;; + let shared_implicit = [Cic.Implicit None] let rec path_string_of_term = function - | Cic.Meta _ -> [Cic.Implicit None] + | Cic.Meta _ -> shared_implicit | Cic.Appl ((hd::tl) as l) -> if not (Hashtbl.mem arities hd) then Hashtbl.add arities hd (List.length tl); -- 2.39.2