diff options
| author | corbinea | 2003-06-15 17:21:37 +0000 |
|---|---|---|
| committer | corbinea | 2003-06-15 17:21:37 +0000 |
| commit | 6df339ed3ed3fb7dfa8f63b0f7e33a43daa26249 (patch) | |
| tree | 6776b2b7db5f3a6e93ec17796c696eaeb27b96dd /contrib/first-order/sequent.ml | |
| parent | 74d595d367782c448e69616e65e425f065887f7f (diff) | |
Ground major update ... mmm, sounds exciting !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4167 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/first-order/sequent.ml')
| -rw-r--r-- | contrib/first-order/sequent.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 4942503c6a..4c18090b93 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -31,7 +31,6 @@ let priority = (* pure heuristics, <=0 for non reversible *) | Ror -> -15 | Rfalse -> -50 (* dead end for sure *) | Rforall -> 100 - | Revaluable _ -> 100 | Rexists (_,_,_) -> -30 end | Left lf -> @@ -41,7 +40,6 @@ let priority = (* pure heuristics, <=0 for non reversible *) | Lor _ -> 40 | Lforall (_,_,_) -> -30 (* must stay at lowest priority *) | Lexists _ -> 60 - | Levaluable _ -> 100 | LA(_,lap) -> match lap with LLatom -> 0 @@ -51,7 +49,6 @@ let priority = (* pure heuristics, <=0 for non reversible *) | LLforall _ -> -20 | LLexists (_,_) -> 50 | LLarrow (_,_,_) -> -10 - | LLevaluable _ -> 100 let left_reversible lpat=(priority lpat)>0 |