]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_proof_checking/cicPp.ml
added annotations to Cic.Implicit
[helm.git] / helm / ocaml / cic_proof_checking / cicPp.ml
index 152cdd19835f602987b34bb762987cdb481b3d09..b0e7d64ed31be5f58e6c3c095b29eac6a845ee70 100644 (file)
@@ -88,7 +88,7 @@ let rec pp t l =
          | C.Type  -> "Type"
         | C.CProp -> "CProp" 
        )
-    | C.Implicit -> "?"
+    | C.Implicit -> "?"
     | C.Prod (b,s,t) ->
        (match b with
           C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)