diff options
| -rw-r--r-- | Makefile.common | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 8 | ||||
| -rw-r--r-- | library/summary.mli | 6 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 2 |
4 files changed, 15 insertions, 5 deletions
diff --git a/Makefile.common b/Makefile.common index a74126dfe..0b714d1f6 100644 --- a/Makefile.common +++ b/Makefile.common @@ -344,9 +344,9 @@ CONTRIBSTATIC:=\ $(FUNINDCMO) ifneq ($(HASNATDYNLINK),false) - CONTRIBSTATIC:=$(SUBTACCMO) + CONTRIBSTATIC:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ - $(XMLCMA) $(FUNINDCMA) #$(SUBTACCMA) + $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) PLUGINS:=$(INITPLUGINS) \ $(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) \ $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \ diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 839597ece..df700e1b1 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; diff --git a/library/summary.mli b/library/summary.mli index 7f300a996..3e6375b0e 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -28,5 +28,9 @@ val section_unfreeze_summaries : frozen -> unit val module_unfreeze_summaries : frozen -> unit val init_summaries : unit -> unit - +(** Beware: if some code is dynamically loaded via dynlink after the + initialization of Coq, the init functions of any summary declared + by this code may not be run. It is hence the responsability of + plugins to initialize themselves properly. +*) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index d1910c145..9bac42c93 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -231,7 +231,7 @@ let stdlib_use_plugins = Coq_config.has_natdynlink let initial_plugins = [ "Extraction_plugin"; "Cc_plugin"; "Ground_plugin"; "Dp_plugin"; - "Recdef_plugin"; (*"subtac_plugin";*) "Xml_plugin"; ] + "Recdef_plugin"; "Subtac_plugin"; "Xml_plugin"; ] (** Other plugins of the standard library. We need their list to avoid trying to load them if they have been statically compiled |