diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:34:09 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:34:09 +0000 |
| commit | 1a1ee340de86b6688a8ceeec5eaa8e76032fe3f3 (patch) | |
| tree | 977ac085e6b783933d316b3ff4eef1fba3d4dda9 /proofs/goal.ml | |
| parent | fed5cbc5b006447bb3d877b3eeb35f7c76e96661 (diff) | |
Getting rid of Goal.here, and all the related exceptions and combinators.
It was a bad idea. The new API based on lists seems more sensible.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 33 |
1 files changed, 0 insertions, 33 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 988c10d27..da5cb6b19 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -352,39 +352,6 @@ let env env _ _ _ = env let defs _ rdefs _ _ = !rdefs -(* Cf mli for more detailed comment. - [null], [plus], [here] and [here_list] use internal exception [UndefinedHere] - to communicate whether or not the value is defined in the particular context. *) -exception UndefinedHere -(* no handler: this should never be allowed to reach toplevel *) -let null _ _ _ _ = raise UndefinedHere - -let plus s1 s2 env rdefs goal info = - try s1 env rdefs goal info - with UndefinedHere -> s2 env rdefs goal info - -(* Equality of two goals *) -let equal_pointer { content = e1 } { content = e2 } = Evar.equal e1 e2 - -let here goal value _ _ goal' _ = - if equal_pointer goal goal' then - value - else - raise UndefinedHere - -(* arnaud: voir à la passer dans Util ? *) -let rec list_mem_with eq x = function - | y::_ when eq x y -> true - | _::l -> list_mem_with eq x l - | [] -> false - -let here_list goals value _ _ goal' _ = - if list_mem_with equal_pointer goal' goals then - value - else - raise UndefinedHere - - (*** Conversion in goals ***) let convert_hyp check (id,b,bt as d) env rdefs gl info = |