- match interp id with
- None -> raise (UnknownIdentifier id)
- | Some (CicTextualParser0.IndTyUri (uri,tyno)) -> (uri,tyno)
- | Some _ -> raise InductiveTypeURIExpected
+ let module CTP0 = CicTextualParser0 in
+ match interp id with
+ None -> raise (UnknownIdentifier id)
+ | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno)) -> (uri,tyno)
+ | Some _ -> raise InductiveTypeURIExpected
+ ;;
+
+ let mk_implicit () =
+ let newmeta = new_meta () in
+ let new_canonical_context = [] in
+ let irl =
+ identity_relocation_list_for_metavariable new_canonical_context
+ in
+ CicTextualParser0.metasenv :=
+ [newmeta, new_canonical_context, Sort Type ;
+ newmeta+1, new_canonical_context, Meta (newmeta,irl);
+ newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
+ ] @ !CicTextualParser0.metasenv ;
+ [], function _ -> Meta (newmeta+2,irl)