diff options
Diffstat (limited to 'engine/eConstr.mli')
| -rw-r--r-- | engine/eConstr.mli | 32 |
1 files changed, 19 insertions, 13 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 28c9dd3c2..b0e834b2e 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -13,7 +13,7 @@ open Names open Constr open Environ -type t +type t = Evd.econstr (** Type of incomplete terms. Essentially a wrapper around {!Constr.t} ensuring that {!Constr.kind} does not observe defined evars. *) @@ -68,11 +68,14 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -val to_constr : Evd.evar_map -> t -> Constr.t -(** Returns the evar-normal form of the argument, and cast it as a theoretically - evar-free term. In practice this function does not check that the result - is actually evar-free, it is currently the duty of the caller to do so. - This might change in the future. *) +val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t +(** Returns the evar-normal form of the argument. Note that this + function is supposed to be called when the original term has not + more free-evars anymore. If you need compatibility with the old + semantics, set [abort_on_undefined_evars] to [false]. + + For getting the evar-normal form of a term with evars see + {!Evarutil.nf_evar}. *) val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type @@ -108,7 +111,7 @@ val mkLetIn : Name.t * t * t * t -> t val mkApp : t * t array -> t val mkConst : Constant.t -> t val mkConstU : Constant.t * EInstance.t -> t -val mkProj : (projection * t) -> t +val mkProj : (Projection.t * t) -> t val mkInd : inductive -> t val mkIndU : inductive * EInstance.t -> t val mkConstruct : constructor -> t @@ -173,7 +176,7 @@ val destEvar : Evd.evar_map -> t -> t pexistential val destInd : Evd.evar_map -> t -> inductive * EInstance.t val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t val destCase : Evd.evar_map -> t -> case_info * t * t * t array -val destProj : Evd.evar_map -> t -> projection * t +val destProj : Evd.evar_map -> t -> Projection.t * t val destFix : Evd.evar_map -> t -> (t, t) pfixpoint val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint @@ -198,11 +201,11 @@ val whd_evar : Evd.evar_map -> constr -> constr val eq_constr : Evd.evar_map -> t -> t -> bool val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool -val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option -val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option +val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option +val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option (** [eq_constr_universes_proj] can equate projections and their eta-expanded constant form. *) -val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option +val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool @@ -281,12 +284,13 @@ val map_rel_context_in_env : (* XXX Missing Sigma proxy *) val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> - Evd.evar_map -> Globnames.global_reference -> Evd.evar_map * t + Evd.evar_map -> GlobRef.t -> Evd.evar_map * t -val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool +val is_global : Evd.evar_map -> GlobRef.t -> t -> bool (** {5 Extra} *) +val of_existential : Constr.existential -> existential val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, types) Context.Rel.Declaration.pt @@ -305,6 +309,8 @@ sig val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt (** Physical identity. Does not care for defined evars. *) + val to_named_context : (t, types) Context.Named.pt -> Context.Named.t + val to_sorts : ESorts.t -> Sorts.t (** Physical identity. Does not care for normalization. *) |