diff options
| author | letouzey | 2011-05-17 20:13:21 +0000 |
|---|---|---|
| committer | letouzey | 2011-05-17 20:13:21 +0000 |
| commit | 7e52f7728dcfcede7e40455385f3eef05a499c0d (patch) | |
| tree | 1e3ce498a644e7ca6a338b3aa0fc7b32a5f2b7b0 | |
| parent | 7386d0718f8c1e6fb47eea787d4287338f9e7060 (diff) | |
Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14135 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/class_tactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 16e38598b5..870e05e4b7 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -259,7 +259,7 @@ let make_autogoal_hints = fun only_classes ?(st=full_transparent_state) g -> let sign = pf_filtered_hyps g in match !res with - | Some (sign', hints) when sign = sign' -> hints + | Some (sign', hints) when Environ.eq_named_context_val sign sign' -> hints | _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in res := Some (sign, hints); hints |