aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 43fef8685d..a609dd66c3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1391,7 +1391,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
| None -> Id.of_string "__"
| Some id -> id
in
- GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l)
+ GEvar (id,List.map (fun (id,c) -> (CAst.make id, glob_of_pat avoid env sigma c)) l)
| PRel n ->
let id = try match lookup_name_of_rel n env with
| Name id -> id