diff options
| author | herbelin | 2006-05-23 21:51:59 +0000 |
|---|---|---|
| committer | herbelin | 2006-05-23 21:51:59 +0000 |
| commit | e24d8149c3aefd11b03458b6f9b3e38ca454b07a (patch) | |
| tree | 7c66dda6b63ea0c1f3e6e03259ef0b1609aca8b6 /dev/doc/check-grammar | |
| parent | b65fd67d6210f480eed759d58422ca8c4da95eab (diff) | |
Restructuration dossier dev et mise à jour de certaines documentations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/doc/check-grammar')
| -rwxr-xr-x | dev/doc/check-grammar | 50 |
1 files changed, 0 insertions, 50 deletions
diff --git a/dev/doc/check-grammar b/dev/doc/check-grammar deleted file mode 100755 index 67da1bc513..0000000000 --- a/dev/doc/check-grammar +++ /dev/null @@ -1,50 +0,0 @@ -#!/bin/bash -# This scripts checks that the new grammar of Coq as defined in syntax-v8.tex -# is consistent in the sense that all invoked non-terminals are defined - -defined-nt() { - grep "\\DEFNT{.*}" syntax-v8.tex | sed -e "s|.*DEFNT{\([^}]*\)}.*|\1|"|\ - sort | sort -u -} - -used-nt() { - cat syntax-v8.tex | tr \\\\ \\n | grep "^NT{.*}" |\ - sed -e "s|^NT{\([^}]*\)}.*|\1|" | egrep -v ^\#1\|non-terminal | sort -u -} - -used-term() { - cat syntax-v8.tex | tr \\\\ \\n | grep "^TERM{.*}" |\ - sed -e "s|^TERM{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1\|terminal | sort -u -} - -used-kwd() { - cat syntax-v8.tex | tr \\\\ \\n | grep "^KWD{.*}" |\ - sed -e "s|^KWD{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1 | sort -u -} - -defined-nt > def -used-nt > use -used-term > use-t -used-kwd > use-k -diff def use > df - -############################### -echo -if grep ^\> df > /dev/null 2>&1 ; then - echo Undefined non-terminals: - echo ======================== - echo - grep ^\> df | sed -e "s|^> ||" - echo -fi -if grep ^\< df > /dev/null 2>&1 ; then - echo Unused non-terminals: - echo ===================== - echo - grep ^\< df | sed -e "s|^< ||" - echo -fi -#echo Used terminals: -#echo =============== -#echo -#cat use-t
\ No newline at end of file |
