diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-25 17:39:12 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-25 17:39:12 +0000 |
| commit | de5bd6a09e2323faf4ac4b7576d55c3d2cb94ba7 (patch) | |
| tree | 9814cef64f85ad6921b51fba5e489d9bd6cfa507 /proofs/proof.ml | |
| parent | b35582012e9f7923ca2e55bfbfae9215770f8fbd (diff) | |
Monomorphization (proof)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16002 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index bae5f1157..479ccabcc 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -29,6 +29,8 @@ Therefore the undo stack stores action to be ran to undo. *) +open Util + type _focus_kind = int type 'a focus_kind = _focus_kind type focus_info = Obj.t @@ -48,7 +50,7 @@ let new_focus_kind () = r (* Auxiliary function to define conditions. *) -let check kind1 kind2 = kind1=kind2 +let check kind1 kind2 = Int.equal kind1 kind2 (* To be authorized to unfocus one must meet the condition prescribed by the action which focused.*) @@ -85,7 +87,7 @@ module Cond = struct | _ , Cannot e -> Cannot e | Strict, Strict -> Strict | _ , _ -> Loose - let kind e k0 k p = bool e (k0=k) k p + let kind e k0 k p = bool e (Int.equal k0 k) k p let pdone e k p = bool e (Proofview.finished p) k p end |