diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:19 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:19 +0000 |
| commit | d284deddaf736d2387a79b219f328915bc12614c (patch) | |
| tree | c335d0d3de81f75bdb93b5cf6b2a033d51b6475a /toplevel/vernac.mli | |
| parent | db7b19f0f1d6b18bcc62fbedccad7a56f72315f2 (diff) | |
raise UnsafeSuccess -> feedback AddedAxiom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernac.mli')
| -rw-r--r-- | toplevel/vernac.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 9ef3bc28a..379194945 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -26,9 +26,7 @@ val just_parsing : bool ref Backtrack stack (triggering a save of a frozen state and the generation of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -(* spiwack: return value: [true] if safe (general case), [false] if - unsafe (like [Admitted]). *) -val eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> bool +val eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit (** Set XML hooks *) val set_xml_start_library : (unit -> unit) -> unit |