]> matita.cs.unibo.it Git - helm.git/commitdiff
a bit of shareing
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Apr 2006 13:24:35 +0000 (13:24 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Apr 2006 13:24:35 +0000 (13:24 +0000)
helm/software/components/cic/discrimination_tree.ml

index bab98921df04691b090c6e8e3020de76e5ccf5bb..18bc73eb5447280d159c54d087a434468c4b90e6 100644 (file)
@@ -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);