diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/_tags | 44 | ||||
| -rw-r--r-- | plugins/cc/cc_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/dp/dp_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/extraction/extraction_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/field/field_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/firstorder/ground_plugin.mllib | 3 | ||||
| -rw-r--r-- | plugins/fourier/fourier_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/funind/recdef_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/groebner/groebner_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/interface/coqinterface_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/interface/coqparser_plugin.mllib | 3 | ||||
| -rw-r--r-- | plugins/micromega/micromega_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/omega/omega_plugin.mllib | 3 | ||||
| -rw-r--r-- | plugins/quote/quote_plugin.mllib | 3 | ||||
| -rw-r--r-- | plugins/ring/ring_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/romega/romega_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/rtauto/rtauto_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/subtac/subtac_plugin.mllib | 1 | ||||
| -rw-r--r-- | plugins/xml/xml_plugin.mllib | 1 |
20 files changed, 67 insertions, 4 deletions
diff --git a/plugins/_tags b/plugins/_tags new file mode 100644 index 0000000000..a8291f6c8d --- /dev/null +++ b/plugins/_tags @@ -0,0 +1,44 @@ + +"romega/g_romega.ml4": use_grammar +"cc/g_congruence.ml4": use_grammar +"setoid_ring/newring.ml4": use_grammar +"dp/g_dp.ml4": use_grammar +"interface/centaur.ml4": use_grammar +"interface/debug_tac.ml4": use_grammar +"quote/g_quote.ml4": use_grammar +"subtac/equations.ml4": use_grammar +"subtac/g_eterm.ml4": use_grammar +"subtac/g_subtac.ml4": use_grammar +"rtauto/g_rtauto.ml4": use_grammar +"xml/xmlentries.ml4": use_grammar +"xml/dumptree.ml4": use_grammar +"firstorder/g_ground.ml4": use_grammar +"omega/g_omega.ml4": use_grammar +"micromega/g_micromega.ml4": use_grammar +"funind/g_indfun.ml4": use_grammar +"field/field.ml4": use_grammar +"extraction/g_extraction.ml4": use_grammar +"ring/g_ring.ml4": use_grammar +"fourier/g_fourier.ml4": use_grammar +"groebner/groebner.ml4": use_grammar + + +"cc": include +"extraction": include +"firstorder": include +"funind": include +"interface": include +"micromega": include +"quote": include +"romega": include +"setoid_ring": include +"xml": include +"dp": include +"field": include +"fourier": include +"groebner": include +"jprover": include +"omega": include +"ring": include +"rtauto": include +"subtac": include
\ No newline at end of file diff --git a/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mllib index 27e903fd38..1bcfc5378b 100644 --- a/plugins/cc/cc_plugin.mllib +++ b/plugins/cc/cc_plugin.mllib @@ -2,3 +2,4 @@ Ccalgo Ccproof Cctac G_congruence +Cc_plugin_mod diff --git a/plugins/dp/dp_plugin.mllib b/plugins/dp/dp_plugin.mllib index 361d6f8323..adb9721a19 100644 --- a/plugins/dp/dp_plugin.mllib +++ b/plugins/dp/dp_plugin.mllib @@ -3,3 +3,4 @@ Dp_zenon Dp Dp_gappa G_dp +Dp_plugin_mod diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib index bb87b9e325..b7f458611a 100644 --- a/plugins/extraction/extraction_plugin.mllib +++ b/plugins/extraction/extraction_plugin.mllib @@ -8,3 +8,4 @@ Haskell Scheme Extract_env G_extraction +Extraction_plugin_mod diff --git a/plugins/field/field_plugin.mllib b/plugins/field/field_plugin.mllib index 63492a64f0..3c3e87af55 100644 --- a/plugins/field/field_plugin.mllib +++ b/plugins/field/field_plugin.mllib @@ -1 +1,2 @@ Field +Field_plugin_mod diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mllib index 863ccb50e8..1647e0f3d3 100644 --- a/plugins/firstorder/ground_plugin.mllib +++ b/plugins/firstorder/ground_plugin.mllib @@ -4,4 +4,5 @@ Sequent Rules Instances Ground -G_ground
\ No newline at end of file +G_ground +Ground_plugin_mod diff --git a/plugins/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mllib index b6262f8aeb..0383b1a80b 100644 --- a/plugins/fourier/fourier_plugin.mllib +++ b/plugins/fourier/fourier_plugin.mllib @@ -1,3 +1,4 @@ Fourier FourierR G_fourier +Fourier_plugin_mod diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mllib index c30ee212f5..31818c3992 100644 --- a/plugins/funind/recdef_plugin.mllib +++ b/plugins/funind/recdef_plugin.mllib @@ -8,3 +8,4 @@ Invfun Indfun Merge G_indfun +Recdef_plugin_mod diff --git a/plugins/groebner/groebner_plugin.mllib b/plugins/groebner/groebner_plugin.mllib index 1da12fcf2e..e227b5e09d 100644 --- a/plugins/groebner/groebner_plugin.mllib +++ b/plugins/groebner/groebner_plugin.mllib @@ -2,3 +2,4 @@ Utile Polynom Ideal Groebner +Groebner_plugin_mod diff --git a/plugins/interface/coqinterface_plugin.mllib b/plugins/interface/coqinterface_plugin.mllib index e4b575b136..abb38cf79e 100644 --- a/plugins/interface/coqinterface_plugin.mllib +++ b/plugins/interface/coqinterface_plugin.mllib @@ -12,3 +12,4 @@ Showproof Blast Depends Centaur +Coqinterface_plugin_mod diff --git a/plugins/interface/coqparser_plugin.mllib b/plugins/interface/coqparser_plugin.mllib index 65ec577153..e00b41c6d9 100644 --- a/plugins/interface/coqparser_plugin.mllib +++ b/plugins/interface/coqparser_plugin.mllib @@ -1,4 +1,5 @@ Line_parser Vtp Xlate -Coqparser
\ No newline at end of file +Coqparser +Coqparser_plugin_mod diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mllib index 41753542f6..518654a45f 100644 --- a/plugins/micromega/micromega_plugin.mllib +++ b/plugins/micromega/micromega_plugin.mllib @@ -4,3 +4,4 @@ Mfourier Certificate Coq_micromega G_micromega +Micromega_plugin_mod diff --git a/plugins/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mllib index 0209013762..2b387fdcee 100644 --- a/plugins/omega/omega_plugin.mllib +++ b/plugins/omega/omega_plugin.mllib @@ -1,3 +1,4 @@ Omega Coq_omega -G_omega
\ No newline at end of file +G_omega +Omega_plugin_mod diff --git a/plugins/quote/quote_plugin.mllib b/plugins/quote/quote_plugin.mllib index 21810acdff..d1b3ccbe1e 100644 --- a/plugins/quote/quote_plugin.mllib +++ b/plugins/quote/quote_plugin.mllib @@ -1,2 +1,3 @@ Quote -G_quote
\ No newline at end of file +G_quote +Quote_plugin_mod diff --git a/plugins/ring/ring_plugin.mllib b/plugins/ring/ring_plugin.mllib index 183884ca6d..3c5f995f71 100644 --- a/plugins/ring/ring_plugin.mllib +++ b/plugins/ring/ring_plugin.mllib @@ -1,2 +1,3 @@ Ring G_ring +Ring_plugin_mod diff --git a/plugins/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mllib index 38d0e94111..1625009d06 100644 --- a/plugins/romega/romega_plugin.mllib +++ b/plugins/romega/romega_plugin.mllib @@ -1,3 +1,4 @@ Const_omega Refl_omega G_romega +Romega_plugin_mod diff --git a/plugins/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mllib index 61c5e945bc..0e34604495 100644 --- a/plugins/rtauto/rtauto_plugin.mllib +++ b/plugins/rtauto/rtauto_plugin.mllib @@ -1,3 +1,4 @@ Proof_search Refl_tauto G_rtauto +Rtauto_plugin_mod diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib index 54b7c8e676..a98392f1e0 100644 --- a/plugins/setoid_ring/newring_plugin.mllib +++ b/plugins/setoid_ring/newring_plugin.mllib @@ -1 +1,2 @@ Newring +Newring_plugin_mod diff --git a/plugins/subtac/subtac_plugin.mllib b/plugins/subtac/subtac_plugin.mllib index 81b9ee2bab..394a4b30fc 100644 --- a/plugins/subtac/subtac_plugin.mllib +++ b/plugins/subtac/subtac_plugin.mllib @@ -12,3 +12,4 @@ Subtac_classes Subtac G_subtac Equations +Subtac_plugin_mod diff --git a/plugins/xml/xml_plugin.mllib b/plugins/xml/xml_plugin.mllib index 3297ff0684..90797e8dd9 100644 --- a/plugins/xml/xml_plugin.mllib +++ b/plugins/xml/xml_plugin.mllib @@ -10,3 +10,4 @@ ProofTree2Xml Xmlentries Cic2Xml Dumptree +Xml_plugin_mod |