From 0e2c8316d4e2b15a0d73535d94250617eba111b0 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 --- helm/software/components/cic/discrimination_tree.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/cic/discrimination_tree.ml b/helm/software/components/cic/discrimination_tree.ml index bab98921d..18bc73eb5 100644 --- a/helm/software/components/cic/discrimination_tree.ml +++ b/helm/software/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.5