diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:14 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:14 +0200 |
| commit | da178a880e3ace820b41d38b191d3785b82991f5 (patch) | |
| tree | 6356ab3164a5ad629f4161dc6c44ead74edc2937 /dev | |
| parent | e4282ea99c664d8d58067bee199cbbcf881b60d5 (diff) | |
Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ocamldebug-coq.template | 2 | ||||
| -rwxr-xr-x | dev/v8-syntax/check-grammar | 18 |
2 files changed, 10 insertions, 10 deletions
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template index 560d06d9..5f49561b 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/contrib/extraction -I $COQTOP/contrib/field \ -I $COQTOP/contrib/fourier -I $COQTOP/contrib/firstorder \ - -I $COQTOP/contrib/interface \ + -I $COQTOP/contrib/interface -I $COQTOP/contrib/cc \ -I $COQTOP/contrib/omega -I $COQTOP/contrib/romega \ -I $COQTOP/contrib/ring -I $COQTOP/contrib/xml \ -I $COQTOP/contrib/subtac -I $COQTOP/contrib/funind \ diff --git a/dev/v8-syntax/check-grammar b/dev/v8-syntax/check-grammar index 67da1bc5..194a55fe 100755 --- a/dev/v8-syntax/check-grammar +++ b/dev/v8-syntax/check-grammar @@ -1,31 +1,31 @@ -#!/bin/bash +#!/bin/sh # 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() { +defined_nt() { grep "\\DEFNT{.*}" syntax-v8.tex | sed -e "s|.*DEFNT{\([^}]*\)}.*|\1|"|\ sort | sort -u } -used-nt() { +used_nt() { cat syntax-v8.tex | tr \\\\ \\n | grep "^NT{.*}" |\ sed -e "s|^NT{\([^}]*\)}.*|\1|" | egrep -v ^\#1\|non-terminal | sort -u } -used-term() { +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() { +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 +defined_nt > def +used_nt > use +used_term > use-t +used_kwd > use-k diff def use > df ############################### |