From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 5 Apr 2006 13:24:35 +0000 (+0000)
Subject: a bit of shareing
X-Git-Tag: make_still_working~7431
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e2c8316d4e2b15a0d73535d94250617eba111b0;p=helm.git

a bit of shareing
---

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);