diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 52765ff12d..9a599c8ab8 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1524,7 +1524,7 @@ let interp_open_constr sigma env c = let interp_open_constr_patvar sigma env c = let raw = intern_gen false sigma env c ~allow_patvar:true in - let sigma = ref (Evd.create_evar_defs sigma) in + let sigma = ref sigma in let evars = ref (Gmap.empty : (identifier,glob_constr) Gmap.t) in let rec patvar_to_evar r = match r with | GPatVar (loc,(_,id)) -> |