if a node has an xref use it for cut and paste, no matter if it have an href as well

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index e9ce2e81ca002ea8572bf46a0e1209279a53a62a..05a15691eb3d478e7e8a0e986babac1adb7640db 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -318,7 +318,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
         Cic.Meta (index, cic_subst)
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
-    | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
+    | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
     | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
@@ -631,7 +631,7 @@ module type Disambiguator =
 sig
   val disambiguate_term :
     ?fresh_instances:bool ->
-    dbd:Mysql.dbd ->
+    dbd:HMysql.dbd ->
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
@@ -646,7 +646,7 @@ sig
 
   val disambiguate_obj :
     ?fresh_instances:bool ->
-    dbd:Mysql.dbd ->
+    dbd:HMysql.dbd ->
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
@@ -690,7 +690,7 @@ module Make (C: Callbacks) =
            fun _ _ _ -> term))
         uris
 
-let refine_profiler = CicUtil.profile "disambiguate_thing.refine_thing"
+let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
     let disambiguate_thing ~dbd ~context ~metasenv
       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
@@ -784,7 +784,7 @@ let refine_profiler = CicUtil.profile "disambiguate_thing.refine_thing"
 let foo () =
           let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
             (k , ugraph1 )
-in refine_profiler.CicUtil.profile foo ()
+in refine_profiler.HExtlib.profile foo ()
         with
         | Try_again -> Uncertain, ugraph
         | Invalid_choice -> Ko, ugraph