From 174922d9d8f206ee4e2e87ebf90dea06613ed2fa Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 22 Nov 2005 18:03:36 +0000 Subject: [PATCH] support pretty printing of Cic.Implicit --- helm/ocaml/cic_notation/cicNotationRew.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 919a07fab..8bbc22e24 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -330,7 +330,8 @@ let ast_of_acic0 term_info acic k = | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set) | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u)) | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp) - | Cic.AImplicit _ -> assert false + | Cic.AImplicit (id, Some `Hole) -> idref id Ast.UserInput + | Cic.AImplicit (id, _) -> idref id Ast.Implicit | Cic.AProd (id,n,s,t) -> let binder_kind = match sort_of_id id with -- 2.39.2