added annotations to Cic.Implicit

[helm.git] / helm / ocaml / cic_unification / cicMkImplicit.ml

diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml
index 1817ac8613873ecd2276fae3da36f156d4afda7e..99e599ab2f6feff6e9bcfe4ce8d6a3d21fe3a3c6 100644 (file)
--- a/helm/ocaml/cic_unification/cicMkImplicit.ml
+++ b/helm/ocaml/cic_unification/cicMkImplicit.ml
@@ -87,7 +87,14 @@ let expand_implicits metasenv context term =
     | Cic.Meta (n,l) -> 
         let metasenv', l' = do_local_context metasenv context l in
         metasenv', Cic.Meta (n, l')
-    | Cic.Implicit ->
+    | Cic.Implicit (Some `Type) ->
+        let (metasenv', idx) = mk_implicit_type metasenv context in
+        let irl = identity_relocation_list_for_metavariable context in
+        metasenv', Cic.Meta (idx, irl)
+    | Cic.Implicit (Some `Closed) ->
+        let (metasenv', idx) = mk_implicit metasenv [] in
+        metasenv', Cic.Meta (idx, [])
+    | Cic.Implicit None ->
         let (metasenv', idx) = mk_implicit metasenv context in
         let irl = identity_relocation_list_for_metavariable context in
         metasenv', Cic.Meta (idx, irl)