]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/cicNotationPp.ml
- Procedural: we specify more unifiers for apply to help higher-order unification
[helm.git] / helm / software / components / acic_content / cicNotationPp.ml
index a835e074f40ff48853d9e957de2b9d5d41d13e21..b2cb12f9280120e595e6c90948b5e47b28f75ac3 100644 (file)
@@ -147,7 +147,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Meta (index, substs) ->
         sprintf "%d[%s]" index
           (String.concat "; "
-            (List.map (function None -> "_" | Some t -> pp_term t) substs))
+            (List.map (function None -> "?" | Some t -> pp_term t) substs))
     | Ast.Num (num, _) -> num
     | Ast.Sort `Set -> "Set"
     | Ast.Sort `Prop -> "Prop"
@@ -358,7 +358,7 @@ let pp_env env =
 let rec pp_cic_appl_pattern = function
   | Ast.UriPattern uri -> UriManager.string_of_uri uri
   | Ast.VarPattern name -> name
-  | Ast.ImplicitPattern -> "_"
+  | Ast.ImplicitPattern -> "?"
   | Ast.ApplPattern aps ->
       sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps))