]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/cicUniv.ml
cicDischarge: new module for discharging the explicit variables occurring in a
[helm.git] / helm / software / components / cic / cicUniv.ml
index 03088410f59e3804a3ad527581fb8baef8f19751..3074f2a78778143141bcb79dd516df2f69af1110 100644 (file)
@@ -357,6 +357,8 @@ type universe_graph = bag * UriManager.UriSet.t * bool
 
 let empty_ugraph = empty_bag, UriManager.UriSet.empty, false
 let oblivion_ugraph = empty_bag, UriManager.UriSet.empty, true
+(* FG: default choice for a ugraph ??? *)
+let default_ugraph = oblivion_ugraph   
 
 let current_index_anon = ref (-1)
 let current_index_named = ref (-1)