aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 18d6c1a5b..9a4f2177f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -552,7 +552,7 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id =
let is_var store pat =
match DAst.get pat with
- | PatVar na -> store na; true
+ | PatVar na -> ignore(store na); true
| _ -> false
let out_var pat =