diff options
| -rw-r--r-- | pretyping/evd.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index ccba1d2cc1..a9b42f052b 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -498,7 +498,8 @@ let create_evar_defs sigma = { sigma with conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty } (* spiwack: tentatively deprecated *) let create_goal_evar_defs sigma = { sigma with - conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty } + (* conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty } *) + metas=Metamap.empty } let empty = { evars=EvarMap.empty; conv_pbs=[]; |