aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-27 16:39:36 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-27 16:47:46 +0200
commita3d7630d74b720b771e880dcf0fcad05de553a6e (patch)
tree9570c13571d7ab136a0b41b9223d246344d6fa7c /engine/evd.mli
parent9cadb903b7c3a3be8014152b293cd5ade3a7c8b7 (diff)
Removing meta_with_name from Evd.
Diffstat (limited to 'engine/evd.mli')
-rw-r--r--engine/evd.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index cfe4adc09..bc81bd818 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -440,7 +440,6 @@ 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.t
-val meta_with_name : evar_map -> Id.t -> metavariable
val meta_declare :
metavariable -> types -> ?name:Name.t -> evar_map -> evar_map
val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map