diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-16 20:40:19 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-16 20:40:19 +0000 |
commit | 99ad573113f5afc8bb5409649843567dee40ba40 (patch) | |
tree | 60af0349abfc1aeb5847734094dabceae8979ad1 | |
parent | b6b9ea6c22107a33121cb2e7f6f89ec82d1bc7d0 (diff) |
first-order --> firstorder (kills a warning about not being a valid id)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10805 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | CREDITS | 6 | ||||
-rw-r--r-- | Makefile.build | 2 | ||||
-rw-r--r-- | Makefile.common | 8 | ||||
-rw-r--r-- | contrib/extraction/CHANGES | 4 | ||||
-rw-r--r-- | contrib/firstorder/formula.ml (renamed from contrib/first-order/formula.ml) | 0 | ||||
-rw-r--r-- | contrib/firstorder/formula.mli (renamed from contrib/first-order/formula.mli) | 0 | ||||
-rw-r--r-- | contrib/firstorder/g_ground.ml4 (renamed from contrib/first-order/g_ground.ml4) | 0 | ||||
-rw-r--r-- | contrib/firstorder/ground.ml (renamed from contrib/first-order/ground.ml) | 0 | ||||
-rw-r--r-- | contrib/firstorder/ground.mli (renamed from contrib/first-order/ground.mli) | 0 | ||||
-rw-r--r-- | contrib/firstorder/instances.ml (renamed from contrib/first-order/instances.ml) | 0 | ||||
-rw-r--r-- | contrib/firstorder/instances.mli (renamed from contrib/first-order/instances.mli) | 0 | ||||
-rw-r--r-- | contrib/firstorder/rules.ml (renamed from contrib/first-order/rules.ml) | 0 | ||||
-rw-r--r-- | contrib/firstorder/rules.mli (renamed from contrib/first-order/rules.mli) | 0 | ||||
-rw-r--r-- | contrib/firstorder/sequent.ml (renamed from contrib/first-order/sequent.ml) | 0 | ||||
-rw-r--r-- | contrib/firstorder/sequent.mli (renamed from contrib/first-order/sequent.mli) | 0 | ||||
-rw-r--r-- | contrib/firstorder/unify.ml (renamed from contrib/first-order/unify.ml) | 0 | ||||
-rw-r--r-- | contrib/firstorder/unify.mli (renamed from contrib/first-order/unify.mli) | 0 | ||||
-rw-r--r-- | dev/ocamldebug-coq.template | 2 | ||||
-rw-r--r-- | dev/ocamlweb-doc/Makefile | 2 | ||||
-rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 |
20 files changed, 13 insertions, 13 deletions
@@ -32,10 +32,10 @@ contrib/dp developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre (LRI, 2005-2008) contrib/extraction - developed by Pierre Letouzey (LRI, 2000-2008) + developed by Pierre Letouzey (LRI, 2000-2004, PPS-Paris7, 2005-now) contrib/field developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001) -contrib/first-order +contrib/firstorder developed by Pierre Corbineau (LRI, 2003-2008) contrib/fourier developed by Loïc Pottier (INRIA-Lemme, 2001) @@ -114,7 +114,7 @@ of the Coq Proof assistant during the indicated time : Benjamin Grégoire (INRIA, 2003-now) Hugo Herbelin (INRIA, 1996-now) Gérard Huet (INRIA, 1985-1997) - Pierre Letouzey (LRI, 2000-2005 & PPS-Paris 7, 2005-now) + Pierre Letouzey (LRI, 2000-2004 & PPS-Paris 7, 2005-now) Pascal Manoury (INRIA, 1993) Micaela Mayero (INRIA, 1997-2002) Claude Marché (INRIA 2003-2004 & LRI, 2004-now) diff --git a/Makefile.build b/Makefile.build index b4880e124..ffe6a2249 100644 --- a/Makefile.build +++ b/Makefile.build @@ -64,7 +64,7 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ -I contrib/xml -I contrib/extraction \ -I contrib/interface -I contrib/fourier \ -I contrib/jprover -I contrib/cc \ - -I contrib/funind -I contrib/first-order \ + -I contrib/funind -I contrib/firstorder \ -I contrib/field -I contrib/subtac -I contrib/rtauto \ -I contrib/recdef diff --git a/Makefile.common b/Makefile.common index 8421d397e..bfabd8021 100644 --- a/Makefile.common +++ b/Makefile.common @@ -281,10 +281,10 @@ RECDEFCMO:=\ contrib/recdef/recdef.cmo FOCMO:=\ - contrib/first-order/formula.cmo contrib/first-order/unify.cmo \ - contrib/first-order/sequent.cmo contrib/first-order/rules.cmo \ - contrib/first-order/instances.cmo contrib/first-order/ground.cmo \ - contrib/first-order/g_ground.cmo + contrib/firstorder/formula.cmo contrib/firstorder/unify.cmo \ + contrib/firstorder/sequent.cmo contrib/firstorder/rules.cmo \ + contrib/firstorder/instances.cmo contrib/firstorder/ground.cmo \ + contrib/firstorder/g_ground.cmo CCCMO:=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \ contrib/cc/g_congruence.cmo diff --git a/contrib/extraction/CHANGES b/contrib/extraction/CHANGES index 83ea4910c..acd1dbda4 100644 --- a/contrib/extraction/CHANGES +++ b/contrib/extraction/CHANGES @@ -346,8 +346,8 @@ Dyade/BDDS boolean tautology checker. Lyon/CIRCUITS multiplication via a modelization of a circuit. Lyon/FIRING-SQUAD print the states of the firing squad. Marseille/CIRCUITS compares integers via a modelization of a circuit. -Nancy/FOUnify unification of two first-orderde deux termes. -Rocq/ARITH/Chinese computation of the chinese remaindering. +Nancy/FOUnify unification of two first-order terms. +Rocq/ARITH/Chinese computation of the chinese remainder. Rocq/COC small coc typechecker. (test by B. Barras, not by me) Rocq/HIGMAN run the proof on one example. Rocq/GRAPHS linear constraints checker in Z. diff --git a/contrib/first-order/formula.ml b/contrib/firstorder/formula.ml index ac32f6abe..ac32f6abe 100644 --- a/contrib/first-order/formula.ml +++ b/contrib/firstorder/formula.ml diff --git a/contrib/first-order/formula.mli b/contrib/firstorder/formula.mli index dca55d0bd..dca55d0bd 100644 --- a/contrib/first-order/formula.mli +++ b/contrib/firstorder/formula.mli diff --git a/contrib/first-order/g_ground.ml4 b/contrib/firstorder/g_ground.ml4 index 3ee1db14c..3ee1db14c 100644 --- a/contrib/first-order/g_ground.ml4 +++ b/contrib/firstorder/g_ground.ml4 diff --git a/contrib/first-order/ground.ml b/contrib/firstorder/ground.ml index a8d5fc2ef..a8d5fc2ef 100644 --- a/contrib/first-order/ground.ml +++ b/contrib/firstorder/ground.ml diff --git a/contrib/first-order/ground.mli b/contrib/firstorder/ground.mli index 3c0e903fd..3c0e903fd 100644 --- a/contrib/first-order/ground.mli +++ b/contrib/firstorder/ground.mli diff --git a/contrib/first-order/instances.ml b/contrib/firstorder/instances.ml index 56cea8e07..56cea8e07 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/firstorder/instances.ml diff --git a/contrib/first-order/instances.mli b/contrib/firstorder/instances.mli index aed2ec83d..aed2ec83d 100644 --- a/contrib/first-order/instances.mli +++ b/contrib/firstorder/instances.mli diff --git a/contrib/first-order/rules.ml b/contrib/firstorder/rules.ml index b6112e653..b6112e653 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/firstorder/rules.ml diff --git a/contrib/first-order/rules.mli b/contrib/firstorder/rules.mli index 1c2c93a49..1c2c93a49 100644 --- a/contrib/first-order/rules.mli +++ b/contrib/firstorder/rules.mli diff --git a/contrib/first-order/sequent.ml b/contrib/firstorder/sequent.ml index fd5972fb7..fd5972fb7 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/firstorder/sequent.ml diff --git a/contrib/first-order/sequent.mli b/contrib/firstorder/sequent.mli index 51db9de16..51db9de16 100644 --- a/contrib/first-order/sequent.mli +++ b/contrib/firstorder/sequent.mli diff --git a/contrib/first-order/unify.ml b/contrib/firstorder/unify.ml index 41a100c2b..41a100c2b 100644 --- a/contrib/first-order/unify.ml +++ b/contrib/firstorder/unify.ml diff --git a/contrib/first-order/unify.mli b/contrib/firstorder/unify.mli index d6cb3a082..d6cb3a082 100644 --- a/contrib/first-order/unify.mli +++ b/contrib/firstorder/unify.mli diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template index 978623ad2..ac5ec1e0d 100644 --- a/dev/ocamldebug-coq.template +++ b/dev/ocamldebug-coq.template @@ -19,7 +19,7 @@ exec $OCAMLDEBUG \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ -I $COQTOP/translate \ -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \ - -I $COQTOP/contrib/fourier -I $COQTOP/contrib/first-order \ + -I $COQTOP/contrib/fourier -I $COQTOP/contrib/firstorder \ -I $COQTOP/contrib/interface -I $COQTOP/contrib/jprover \ -I $COQTOP/contrib/omega -I $COQTOP/contrib/romega \ -I $COQTOP/contrib/ring -I $COQTOP/contrib/xml \ diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile index 5a5b3b975..7ab1bd3fc 100644 --- a/dev/ocamlweb-doc/Makefile +++ b/dev/ocamlweb-doc/Makefile @@ -9,7 +9,7 @@ LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \ -I ../../contrib/xml -I ../../contrib/extraction \ -I ../../contrib/interface -I ../../contrib/fourier \ -I ../../contrib/jprover -I ../../contrib/cc \ - -I ../../contrib/funind -I ../../contrib/first-order \ + -I ../../contrib/funind -I ../../contrib/firstorder \ -I ../../contrib/field -I ../../contrib/subtac -I ../../contrib/rtauto \ -I ../../contrib/recdef diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 97973df2b..de68ce1e5 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -748,7 +748,7 @@ Conflicts exists between integers and constrs. \nlsep \TERM{cc} %% contrib/field \nlsep \TERM{field}~\STAR{\tacconstr} -%% contrib/first-order +%% contrib/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}} |