aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evd.mli')
-rw-r--r--pretyping/evd.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a4e314873..a73dbdcdc 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -217,7 +217,7 @@ val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_
val meta_type : evar_map -> metavariable -> types
val meta_ftype : evar_map -> metavariable -> types freelisted
val meta_name : evar_map -> metavariable -> name
-val meta_with_name : evar_map -> identifier -> metavariable
+val meta_with_name : evar_map -> Id.t -> metavariable
val meta_declare :
metavariable -> types -> ?name:name -> evar_map -> evar_map
val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map