aboutsummaryrefslogtreecommitdiff
path: root/engine/evarutil.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-07-04 18:28:33 +0200
committerPierre-Marie Pédrot2020-08-06 12:33:58 +0200
commit29cc320bc3d54b9b4b8d78240db50cc8a878b033 (patch)
tree079aaddfe31d534b5ea43f10e4c4f00a5e2808d4 /engine/evarutil.mli
parent51ecccef0308eceec1ddd9776a03fd993b3ea71a (diff)
Store the default evar instance inside the evar info.
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 ->