aboutsummaryrefslogtreecommitdiff
path: root/engine/evarutil.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evarutil.mli')
-rw-r--r--engine/evarutil.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 41b58d38b0..8083bb86c3 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -42,6 +42,7 @@ val new_evar :
val new_pure_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+ ?identity:EConstr.t list ->
?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
?typeclass_candidate:bool ->