Allow to turn contrib/subtac into a (nat)dynlink'able plugin

Main issue was declare_summary being triggered too late in
subtac_obligations, hence the associated init_function was
_not_ being done by Lib.init(). Fixed for the moment by
an ad-hoc launch of this init_function in subtac_obligations.

In other plugins, this issue doesn't appear, since
init_function is mostly putting back some empty set into
a reference that was initially empty. No need to really
run init_function in this case. For future plugins, we will
nonetheless have to be careful about that.

Of course, the (ref Obj.magic) was not exactly helpful in
debugging this matter, see http://caml.inria.fr/mantis/view.php?id=4707
As said by Xavier, naughty naughty boys...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11877 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 1 deletions

diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 839597ece8..df700e1b1f 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -63,7 +63,7 @@ let assumption_message id =
   Flags.if_verbose message ((string_of_id id) ^ " is assumed")
 
 let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
-let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ())
+let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId [])
 
 let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
 
@@ -134,6 +134,12 @@ let unfreeze (v, t) = from_prg := v; set_default_tactic t
 let init () =
   from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligation_tactic" [])
 
+(** Beware: if this code is dynamically loaded via dynlink after the start
+    of Coq, then this [init] function will not be run by [Lib.init ()].
+    Luckily, here we can launch [init] at load-time. *)
+
+let _ = init ()
+
 let _ = 
   Summary.declare_summary "program-tcc-table"
     { Summary.freeze_function = freeze;