+ let deoptionize_exp_named_subst =
+ function
+ None -> [], (function _ -> [])
+ | Some (dom,mk_exp_named_subst) -> dom,mk_exp_named_subst
+ ;;
+
+ let term_of_con_uri uri exp_named_subst =
+ Const (uri,exp_named_subst)
+ ;;
+
+ let term_of_var_uri uri exp_named_subst =
+ Var (uri,exp_named_subst)
+ ;;
+
+ let term_of_indty_uri (uri,tyno) exp_named_subst =
+ MutInd (uri, tyno, exp_named_subst)
+ ;;
+
+ let term_of_indcon_uri (uri,tyno,consno) exp_named_subst =
+ MutConstruct (uri, tyno, consno, exp_named_subst)
+ ;;
+
+ let term_of_uri uri =
+ match uri with
+ CicTextualParser0.ConUri uri ->
+ term_of_con_uri uri
+ | CicTextualParser0.VarUri uri ->
+ term_of_var_uri uri
+ | CicTextualParser0.IndTyUri (uri,tyno) ->
+ term_of_indty_uri (uri,tyno)
+ | CicTextualParser0.IndConUri (uri,tyno,consno) ->
+ term_of_indcon_uri (uri,tyno,consno)
+ ;;
+
+ let var_uri_of_id id interp =
+ let module CTP0 = CicTextualParser0 in
+ match interp (CicTextualParser0.Id id) with
+ None -> raise (UnknownIdentifier id)
+ | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri
+ | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
+ ;;
+
+ let indty_uri_of_id id interp =
+ let module CTP0 = CicTextualParser0 in
+ match interp (CicTextualParser0.Id 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)
+ ;;