aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evd.mli')
-rw-r--r--pretyping/evd.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a73dbdcdc..86ec47d3e 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -68,8 +68,8 @@ type instance_status = instance_constraint * instance_typing_status
(** Clausal environments *)
type clbinding =
- | Cltyp of name * constr freelisted
- | Clval of name * (constr freelisted * instance_status) * constr freelisted
+ | Cltyp of Name.t * constr freelisted
+ | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
val map_clb : (constr -> constr) -> clbinding -> clbinding
@@ -216,10 +216,10 @@ val meta_fvalue : evar_map -> metavariable -> constr freelisted * instance_st
val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_status) option
val meta_type : evar_map -> metavariable -> types
val meta_ftype : evar_map -> metavariable -> types freelisted
-val meta_name : evar_map -> metavariable -> name
+val meta_name : evar_map -> metavariable -> Name.t
val meta_with_name : evar_map -> Id.t -> metavariable
val meta_declare :
- metavariable -> types -> ?name:name -> evar_map -> evar_map
+ metavariable -> types -> ?name:Name.t -> evar_map -> evar_map
val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map
val meta_reassign : metavariable -> constr * instance_status -> evar_map -> evar_map