diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-13 09:38:47 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-13 12:08:33 +0200 |
commit | c272523bb9d89fe55d1636b48728e7938a8230dd (patch) | |
tree | 6a9b4eee3169298d9371c76558189c1d0b27a2d4 /tactics/tactics.ml | |
parent | 54b1d23e062940263b6868945db808d49d011306 (diff) |
Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).
Diffstat (limited to 'tactics/tactics.ml')
0 files changed, 0 insertions, 0 deletions