aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_vernac.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_vernac.ml4')
-rw-r--r--parsing/g_vernac.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4a59b8597..819d236cd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -131,7 +131,7 @@ let test_plural_form_types loc kwd = function
let fresh_var env c =
Namegen.next_ident_away (Id.of_string "pat")
- (env @ Id.Set.elements (Topconstr.free_vars_of_constr_expr c))
+ (List.fold_left (fun accu id -> Id.Set.add id accu) (Topconstr.free_vars_of_constr_expr c) env)
let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var