| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
- | `Set | `Type _ -> `Pi
+ | `Set | `Type _ | `NType _ -> `Pi
| `Prop | `CProp _ -> `Forall
in
idref id (Ast.Binder (binder_kind,
let _ = load_patterns32 []
-let instantiate_appl_pattern env appl_pattern =
+let instantiate_appl_pattern
+ ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern
+=
let lookup name =
try List.assoc name env
with Not_found ->
assert false
in
let rec aux = function
- | Ast.UriPattern uri -> CicUtil.term_of_uri uri
- | Ast.ImplicitPattern -> Cic.Implicit None
+ | Ast.UriPattern uri -> term_of_uri uri
+ | Ast.ImplicitPattern -> mk_implicit false
| Ast.VarPattern name -> lookup name
- | Ast.ApplPattern terms -> Cic.Appl (List.map aux terms)
+ | Ast.ApplPattern terms -> mk_appl (List.map aux terms)
in
aux appl_pattern