X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=487bceb871377cfb1964e94ad81cccf878e8d733;hb=8a218c35f9bde765a73f14867a294c874f9dc15c;hp=f221a2b05a57a31596ab767c2a8438f1d40a919c;hpb=2f67829c12dea538114bb848e0275d220dba601b;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index f221a2b05..487bceb87 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -419,7 +419,7 @@ let new_flavour_of_flavour = function
   | `MutualDefinition -> `Definition 
   | `Fact -> `Fact
   | `Lemma -> `Lemma
-  | `Remark -> `Corollary
+  | `Remark -> `Example
   | `Theorem -> `Theorem
   | `Variant -> `Corollary 
   | `Axiom -> `Fact
@@ -614,7 +614,7 @@ let interpretate_obj
 ;;
 
 let disambiguate_term ~context ~metasenv ~subst ~expty
-   ~mk_implicit ~description_of_alias ~mk_choice
+   ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
    ~aliases ~universe ~rdb ~lookup_in_library 
    (text,prefix_len,term) 
  =
@@ -623,7 +623,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_term
      ~context ~metasenv ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias
+     ~mk_implicit ~description_of_alias ~fix_instance
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
      ~passes:(MultiPassDisambiguator.passes ())
@@ -636,7 +636,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
 ;;
 
 let disambiguate_obj 
-   ~mk_implicit ~description_of_alias ~mk_choice
+   ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
    ~aliases ~universe ~rdb ~lookup_in_library ~uri
    (text,prefix_len,obj) 
  =
@@ -645,7 +645,7 @@ let disambiguate_obj
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_obj
      ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias
+     ~mk_implicit ~description_of_alias ~fix_instance
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe 
      ~uri:(Some uri)