aboutsummaryrefslogtreecommitdiff
path: root/engine/sigma.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-11-30 00:33:08 +0100
committerPierre-Marie Pédrot2017-02-14 17:30:44 +0100
commit1683b718f85134fdb0d49535e489344e1a7d56f5 (patch)
tree5750652739a4c80c793573b29bc8f73194ed1a7f /engine/sigma.mli
parent27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 (diff)
Making Evd independent from Namegen.
Diffstat (limited to 'engine/sigma.mli')
-rw-r--r--engine/sigma.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/sigma.mli b/engine/sigma.mli
index 7473a251b7..8e8df02f29 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -61,7 +61,7 @@ val to_evar : 'r evar -> Evar.t
type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
-val new_evar : 'r t -> ?naming:Misctypes.intro_pattern_naming_expr ->
+val new_evar : 'r t -> ?name:Id.t ->
Evd.evar_info -> 'r fresh
val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma