diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 2 | ||||
| -rw-r--r-- | API/API.mli | 78 |
2 files changed, 65 insertions, 15 deletions
diff --git a/API/API.ml b/API/API.ml index 46ad36d36d..bf99d0febd 100644 --- a/API/API.ml +++ b/API/API.ml @@ -212,7 +212,7 @@ module Pputils = Pputils module Ppconstr = Ppconstr module Printer = Printer (* module Printmod *) -(* module Prettyp *) +module Prettyp = Prettyp module Ppvernac = Ppvernac (******************************************************************************) diff --git a/API/API.mli b/API/API.mli index 654d934856..04c69b025f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1795,6 +1795,7 @@ sig val pr_path : full_path -> Pp.t val make_path : Names.DirPath.t -> Names.Id.t -> full_path val eq_full_path : full_path -> full_path -> bool + val repr_path : full_path -> Names.DirPath.t * Names.Id.t val dirpath : full_path -> Names.DirPath.t val path_of_string : string -> full_path @@ -1935,24 +1936,19 @@ module Nametab : sig exception GlobalizationError of Libnames.qualid - type ltac_constant = Names.KerName.t - val global : Libnames.reference -> Globnames.global_reference val global_of_path : Libnames.full_path -> Globnames.global_reference val shortest_qualid_of_global : Names.Id.Set.t -> Globnames.global_reference -> Libnames.qualid val path_of_global : Globnames.global_reference -> Libnames.full_path val locate_extended : Libnames.qualid -> Globnames.extended_global_reference val full_name_module : Libnames.qualid -> Names.DirPath.t - val locate_tactic : Libnames.qualid -> Names.KerName.t val pr_global_env : Names.Id.Set.t -> Globnames.global_reference -> Pp.t - val shortest_qualid_of_tactic : Names.KerName.t -> Libnames.qualid val basename_of_global : Globnames.global_reference -> Names.Id.t type visibility = | Until of int | Exactly of int - val push_tactic : visibility -> Libnames.full_path -> Names.KerName.t -> unit val error_global_not_found : ?loc:Loc.t -> Libnames.qualid -> 'a val shortest_qualid_of_module : Names.ModPath.t -> Libnames.qualid val dirpath_of_module : Names.ModPath.t -> Names.DirPath.t @@ -1960,6 +1956,40 @@ sig val dirpath_of_global : Globnames.global_reference -> Names.DirPath.t val locate : Libnames.qualid -> Globnames.global_reference val locate_constant : Libnames.qualid -> Names.Constant.t + + (** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *) + + module type UserName = sig + type t + val equal : t -> t -> bool + val to_string : t -> string + val repr : t -> Names.Id.t * Names.Id.t list + end + + module type EqualityType = + sig + type t + val equal : t -> t -> bool + end + + module type NAMETREE = sig + type elt + type t + type user_name + + val empty : t + val push : visibility -> user_name -> elt -> t -> t + val locate : Libnames.qualid -> t -> elt + val find : user_name -> t -> elt + val exists : user_name -> t -> bool + val user_name : Libnames.qualid -> t -> user_name + val shortest_qualid : Names.Id.Set.t -> user_name -> t -> Libnames.qualid + val find_prefixes : Libnames.qualid -> t -> elt list + end + + module Make (U : UserName) (E : EqualityType) : + NAMETREE with type user_name = U.t and type elt = E.t + end module Global : @@ -2751,15 +2781,15 @@ sig the whole identifier except for the {i subscript}. E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *) - val next_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string val id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t - val next_ident_away_in_goal : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_ident_away_in_goal : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val default_dependent_ident : Names.Id.t - val next_global_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_global_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val rename_bound_vars_as_displayed : - Evd.evar_map -> Names.Id.t list -> Names.Name.t list -> EConstr.types -> EConstr.types + Evd.evar_map -> Names.Id.Set.t -> Names.Name.t list -> EConstr.types -> EConstr.types end module Termops : @@ -3670,7 +3700,7 @@ sig type lname = Names.Name.t Loc.located type lident = Names.Id.t Loc.located type opacity_flag = - | Opaque of lident list option + | Opaque | Transparent type locality_flag = bool type inductive_kind = @@ -4011,7 +4041,7 @@ sig | Later : [ `thunk ] delay val print_universes : bool ref val print_evar_arguments : bool ref - val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.t list -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g + val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.Set.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit end @@ -4628,8 +4658,10 @@ sig val pf_env : 'a Proofview.Goal.t -> Environ.env val pf_ids_of_hyps : 'a Proofview.Goal.t -> Names.Id.t list + val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Names.Id.Set.t val pf_concl : 'a Proofview.Goal.t -> EConstr.types val pf_get_new_id : Names.Id.t -> 'a Proofview.Goal.t -> Names.Id.t + val pf_get_hyp : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.named_declaration val pf_get_hyp_typ : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.types val pf_get_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types val pf_global : Names.Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference @@ -4974,6 +5006,21 @@ sig val pr_transparent_state : Names.transparent_state -> Pp.t end +module Prettyp : +sig + type 'a locatable_info = { + locate : Libnames.qualid -> 'a option; + locate_all : Libnames.qualid -> 'a list; + shortest_qualid : 'a -> Libnames.qualid; + name : 'a -> Pp.t; + print : 'a -> Pp.t; + about : 'a -> Pp.t; + } + + val register_locatable : string -> 'a locatable_info -> unit + val print_located_other : string -> Libnames.reference -> Pp.t +end + (************************************************************************) (* End of modules from printing/ *) (************************************************************************) @@ -5140,7 +5187,7 @@ sig val convert_concl : ?check:bool -> EConstr.types -> Constr.cast_kind -> unit tactic val intro_using : Names.Id.t -> unit tactic val intro : unit tactic - val fresh_id_in_env : Names.Id.t list -> Names.Id.t -> Environ.env -> Names.Id.t + val fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t val is_quantified_hypothesis : Names.Id.t -> 'a Goal.t -> bool val tclABSTRACT : ?opaque:bool -> Names.Id.t option -> unit Proofview.tactic -> unit Proofview.tactic val intro_patterns : bool -> Tactypes.intro_patterns -> unit Proofview.tactic @@ -5240,7 +5287,7 @@ sig val eapply_with_bindings : EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic val assert_by : Names.Name.t -> EConstr.types -> unit Proofview.tactic -> unit Proofview.tactic - val intro_avoiding : Names.Id.t list -> unit Proofview.tactic + val intro_avoiding : Names.Id.Set.t -> unit Proofview.tactic val pose_proof : Names.Name.t -> EConstr.constr -> unit Proofview.tactic val pattern_option : (Locus.occurrences * EConstr.constr) list -> Locus.goal_location -> unit Proofview.tactic val compute_elim_sig : Evd.evar_map -> ?elimc:EConstr.constr Misctypes.with_bindings -> EConstr.types -> elim_scheme @@ -5767,8 +5814,11 @@ end module Stm : sig + type doc type state - val state_of_id : + + val get_doc : Feedback.doc_id -> doc + val state_of_id : doc:doc -> Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] end |