aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-13 09:38:47 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-13 12:08:33 +0200
commitc272523bb9d89fe55d1636b48728e7938a8230dd (patch)
tree6a9b4eee3169298d9371c76558189c1d0b27a2d4 /tactics/tactics.ml
parent54b1d23e062940263b6868945db808d49d011306 (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