added annotations to Cic.Implicit

[helm.git] / helm / ocaml / cic_omdoc / cic2acic.ml

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index f7c2317ba660985d0d44285fe12e750b7a002e50..8418a64d42506796fc8afb5d245e12415c7c7869 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -203,7 +203,7 @@ Cic.Sort Cic.Type ;
                   | Some _, None -> assert false (* due to typing rules *))
                 canonical_context l))
           | C.Sort s -> C.ASort (fresh_id'', s)
-          | C.Implicit -> C.AImplicit (fresh_id'')
+          | C.Implicit annotation -> C.AImplicit (fresh_id'', annotation)
           | C.Cast (v,t) ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop" then