Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs

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

4 files changed, 26 insertions, 26 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 5aadfa592..a9673664a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -344,7 +344,7 @@ Proof_type: subproof field in type proof_tree glued with the ref field
 
 Tacmach: no more echo from functions of module Refiner
 
-Files contrib/*/g_*.ml4 take the place of files contrib/*/*.v.
+Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v.
 Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd
   VERNAC COMMAND EXTEND macros
 File syntax/PPTactic.v moved to parsing/pptactic.ml
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 560d06d96..2598d6df1 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -17,13 +17,13 @@ exec $OCAMLDEBUG \
 	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
-        -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \
-        -I $COQTOP/contrib/fourier    -I $COQTOP/contrib/firstorder \
-        -I $COQTOP/contrib/interface \
-        -I $COQTOP/contrib/omega      -I $COQTOP/contrib/romega \
-        -I $COQTOP/contrib/ring       -I $COQTOP/contrib/xml \
-	-I $COQTOP/contrib/subtac     -I $COQTOP/contrib/funind \
-        -I $COQTOP/contrib/rtauto     -I $COQTOP/contrib/setoid_ring \
-        -I $COQTOP/contrib/recdef     -I $COQTOP/contrib/dp \
+        -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
+        -I $COQTOP/plugins/fourier    -I $COQTOP/plugins/firstorder \
+        -I $COQTOP/plugins/interface \
+        -I $COQTOP/plugins/omega      -I $COQTOP/plugins/romega \
+        -I $COQTOP/plugins/ring       -I $COQTOP/plugins/xml \
+	-I $COQTOP/plugins/subtac     -I $COQTOP/plugins/funind \
+        -I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
+        -I $COQTOP/plugins/recdef     -I $COQTOP/plugins/dp \
         -I $COQTOP/ide \
 	$*
diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile
index f2c625ed4..8ad226da6 100644
--- a/dev/ocamlweb-doc/Makefile
+++ b/dev/ocamlweb-doc/Makefile
@@ -4,14 +4,14 @@ LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \
 	      -I ../../scripts -I ../../lib -I ../../kernel -I ../../kernel/byterun -I ../../library \
               -I ../../proofs -I ../../tactics -I ../../pretyping \
               -I ../../interp -I ../../toplevel -I ../../parsing -I ../../ide/utils -I ../../ide \
-              -I ../../contrib/omega -I ../../contrib/romega \
-	      -I ../../contrib/ring -I ../../contrib/dp -I ../../contrib/setoid_ring \
-              -I ../../contrib/xml -I ../../contrib/extraction \
-              -I ../../contrib/interface -I ../../contrib/fourier \
-	      -I ../../contrib/cc \
-	      -I ../../contrib/funind -I ../../contrib/firstorder \
-              -I ../../contrib/field -I ../../contrib/subtac -I ../../contrib/rtauto \
-              -I ../../contrib/recdef
+              -I ../../plugins/omega -I ../../plugins/romega \
+	      -I ../../plugins/ring -I ../../plugins/dp -I ../../plugins/setoid_ring \
+              -I ../../plugins/xml -I ../../plugins/extraction \
+              -I ../../plugins/interface -I ../../plugins/fourier \
+	      -I ../../plugins/cc \
+	      -I ../../plugins/funind -I ../../plugins/firstorder \
+              -I ../../plugins/field -I ../../plugins/subtac -I ../../plugins/rtauto \
+              -I ../../plugins/recdef
 
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index de68ce1e5..46ba24da7 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -744,28 +744,28 @@ Conflicts exists between integers and constrs.
 \nlsep \TERM{simplif}
 \nlsep \TERM{intuition}~\OPT{\NTL{tactic}{0}}
 \nlsep \TERM{linearintuition}~\OPT{\NT{num}}
-%% contrib/cc
+%% plugins/cc
 \nlsep \TERM{cc}
-%% contrib/field
+%% plugins/field
 \nlsep \TERM{field}~\STAR{\tacconstr}
-%% contrib/firstorder
+%% plugins/firstorder
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}}
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}}
 %%\nlsep \TERM{gtauto}
 \nlsep \TERM{gintuition}~\OPT{\NTL{tactic}{0}}
-%% contrib/fourier
+%% plugins/fourier
 \nlsep \TERM{fourierZ}
-%% contrib/funind
+%% plugins/funind
 \nlsep \TERM{functional}~\TERM{induction}~\tacconstr~\PLUS{\tacconstr}
-%% contrib/jprover
+%% plugins/jprover
 \nlsep \TERM{jp}~\OPT{\NT{num}}
-%% contrib/omega
+%% plugins/omega
 \nlsep \TERM{omega}
-%% contrib/ring
+%% plugins/ring
 \nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}}
 \nlsep \TERM{ring}~\STAR{\tacconstr}
-%% contrib/romega
+%% plugins/romega
 \nlsep \TERM{romega}
 \SEPDEF
 \DEFNT{orient}