aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evd.ml')
-rw-r--r--pretyping/evd.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 06b3a542d..300b4c8e6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -425,7 +425,7 @@ let evar_define evk body evd =
evars = define evd.evars evk body;
last_mods = evk :: evd.last_mods }
-let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?(filter=None) evd =
+let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
let filter =
if filter = None then
List.map (fun _ -> true) (named_context_of_val hyps)