aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authoraspiwack2013-11-02 15:36:21 +0000
committeraspiwack2013-11-02 15:36:21 +0000
commit49762f64a3616919dbfc1be09410cf830d168e70 (patch)
tree0a0d724fa17fa875b0a1e02b5e948e3760de14fe /kernel
parentdf0d3bbf57f82620d3fafe023ddb63f567b2d269 (diff)
Fix behaviour of the refine tactic with respect to evars in types.
It used not to propagate discovered constraints on the evars of the conclusion of the goal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16987 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions