diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:52:54 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:52:54 +0000 |
| commit | c3ca134628ad4d9ef70a13b65c48ff17c737238f (patch) | |
| tree | 136b4efbc3aefe76dcd2fa772141c774343f46df /interp/constrexpr_ops.mli | |
| parent | 6946bbbf2390024b3ded7654814104e709cce755 (diff) | |
Modulification of name
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 49dea9f31..d857a5b60 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -48,9 +48,9 @@ val mkIdentC : Id.t -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr cast_type -> constr_expr -val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr -val mkLetInC : name located * constr_expr * constr_expr -> constr_expr -val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr +val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr +val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr +val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val prod_constr_expr : constr_expr -> local_binder list -> constr_expr @@ -69,17 +69,17 @@ val coerce_reference_to_id : reference -> Id.t val coerce_to_id : constr_expr -> Id.t located (** Destruct terms of the form [CRef (Ident _)]. *) -val coerce_to_name : constr_expr -> name located +val coerce_to_name : constr_expr -> Name.t located (** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *) (** {6 Binder manipulation} *) val default_binder_kind : binder_kind -val names_of_local_binders : local_binder list -> name located list +val names_of_local_binders : local_binder list -> Name.t located list (** Retrieve a list of binding names from a list of binders. *) -val names_of_local_assums : local_binder list -> name located list +val names_of_local_assums : local_binder list -> Name.t located list (** Same as [names_of_local_binders], but does not take the [let] bindings into account. *) |