diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/core.dbg | 1 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 6 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 2 |
4 files changed, 1 insertions, 9 deletions
diff --git a/dev/base_include b/dev/base_include index e76044f41..2f7183dd6 100644 --- a/dev/base_include +++ b/dev/base_include @@ -15,7 +15,6 @@ #directory "tactics";; #directory "printing";; #directory "grammar";; -#directory "intf";; #directory "stm";; #directory "vernac";; diff --git a/dev/core.dbg b/dev/core.dbg index 57c136900..edf67020a 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -16,5 +16,4 @@ load_printer tactics.cma load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma -load_printer intf.cma load_printer ltac_plugin.cmo diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index b3d49b7e5..764d48295 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -17,12 +17,6 @@ toplevel Special components ------------------ -intf : - - Contains mli-only interfaces, many of them providing a.s.t. - used for dialog bewteen coq components. Ex: Constrexpr.constr_expr - produced by parsing and transformed by interp. - grammar : Camlp5 syntax extensions. The file grammar/grammar.cma is used diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index f3e60edea..8f1c165dd 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -18,7 +18,7 @@ exec $OCAMLDEBUG \ -I $CAMLP5LIB -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ - -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ + -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ |