diff options
| author | ppedrot | 2013-09-27 19:20:27 +0000 |
|---|---|---|
| committer | ppedrot | 2013-09-27 19:20:27 +0000 |
| commit | 11ca3113365639136cf65a74c345080a9434e69b (patch) | |
| tree | da263c149cd1e90bde14768088730e48e78e4776 /proofs/proof.ml | |
| parent | ee2f85396fa0cef65bc4295b5ac6c259e83df134 (diff) | |
Removing a bunch of generic equalities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index c1a909aedc..8ad2458afa 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -66,17 +66,17 @@ end let check_cond_kind c k = let kind_of_cond = function | CondNo (_,k) | CondDone(_,k) | CondEndStack k -> k in - kind_of_cond c = k + Int.equal (kind_of_cond c) k let test_cond c k1 pw = match c with - | CondNo(_, k) when k = k1 -> Strict + | CondNo(_, k) when Int.equal k k1 -> Strict | CondNo(true, _) -> Loose | CondNo(false, _) -> Cannot NotThisWay - | CondDone(_, k) when k = k1 && Proofview.finished pw -> Strict + | CondDone(_, k) when Int.equal k k1 && Proofview.finished pw -> Strict | CondDone(true, _) -> Loose | CondDone(false, _) -> Cannot NotThisWay - | CondEndStack k when k = k1 -> Strict + | CondEndStack k when Int.equal k k1 -> Strict | CondEndStack _ -> Cannot AlreadyNoFocus let no_cond ?(loose_end=false) k = CondNo (loose_end, k) |