diff options
| -rw-r--r-- | .github/CODEOWNERS | 5 | ||||
| -rw-r--r-- | .merlin | 2 | ||||
| -rw-r--r-- | META.coq | 13 | ||||
| -rw-r--r-- | Makefile.common | 4 | ||||
| -rw-r--r-- | configure.ml | 2 | ||||
| -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 | ||||
| -rw-r--r-- | engine/engine.mllib | 1 | ||||
| -rw-r--r-- | engine/evar_kinds.ml (renamed from intf/evar_kinds.ml) | 0 | ||||
| -rw-r--r-- | interp/interp.mllib | 1 | ||||
| -rw-r--r-- | interp/notation_term.ml (renamed from intf/notation_term.ml) | 0 | ||||
| -rw-r--r-- | intf/intf.mllib | 11 | ||||
| -rw-r--r-- | library/decl_kinds.ml (renamed from intf/decl_kinds.ml) | 0 | ||||
| -rw-r--r-- | library/library.mllib | 2 | ||||
| -rw-r--r-- | library/misctypes.ml (renamed from intf/misctypes.ml) | 0 | ||||
| -rw-r--r-- | pretyping/constrexpr.ml (renamed from intf/constrexpr.ml) | 0 | ||||
| -rw-r--r-- | pretyping/extend.ml (renamed from intf/extend.ml) | 0 | ||||
| -rw-r--r-- | pretyping/genredexpr.ml (renamed from intf/genredexpr.ml) | 0 | ||||
| -rw-r--r-- | pretyping/glob_term.ml (renamed from intf/glob_term.ml) | 0 | ||||
| -rw-r--r-- | pretyping/locus.ml (renamed from intf/locus.ml) | 0 | ||||
| -rw-r--r-- | pretyping/pattern.ml (renamed from intf/pattern.ml) | 0 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 9 | ||||
| -rw-r--r-- | pretyping/vernacexpr.ml (renamed from intf/vernacexpr.ml) | 0 |
25 files changed, 16 insertions, 44 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 029b55b9a..7f3ee5c37 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -86,11 +86,6 @@ /interp/ @herbelin # Secondary maintainer @ejgallego -########## Interfaces ########## - -/intf/ @letouzey -# Secondary maintainer @ppedrot - ########## Kernel ########## /kernel/ @maximedenes @@ -10,8 +10,6 @@ S kernel B kernel S kernel/byterun B kernel/byterun -S intf -B intf S library B library S engine @@ -90,19 +90,6 @@ package "library" ( ) -package "intf" ( - - description = "Coq Public Data Types" - version = "8.8" - - requires = "coq.library" - - directory = "intf" - - archive(byte) = "intf.cma" - archive(native) = "intf.cmxa" -) - package "engine" ( description = "Coq Tactic Engine" diff --git a/Makefile.common b/Makefile.common index 9a30e2a4c..eed41fbe7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -75,7 +75,7 @@ INSTALLSH:=./install.sh MKDIR:=install -d CORESRCDIRS:=\ - config clib lib kernel intf kernel/byterun library \ + config clib lib kernel kernel/byterun library \ engine pretyping interp proofs parsing printing \ tactics vernac stm toplevel @@ -102,7 +102,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ # respecting this order is useful for developers that want to load or link # the libraries directly -CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \ +CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ stm/stm.cma toplevel/toplevel.cma diff --git a/configure.ml b/configure.ml index 6c052b63b..2ac705ad2 100644 --- a/configure.ml +++ b/configure.ml @@ -1212,7 +1212,7 @@ let write_configml f = let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "parsing"; "proofs"; - "tactics"; "toplevel"; "printing"; "intf"; + "tactics"; "toplevel"; "printing"; "grammar"; "ide"; "stm"; "vernac" ] in let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") "" 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 \ diff --git a/engine/engine.mllib b/engine/engine.mllib index a3614f6c4..a5df5a9fa 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -2,6 +2,7 @@ Universes Univops UState Nameops +Evar_kinds Evd EConstr Namegen diff --git a/intf/evar_kinds.ml b/engine/evar_kinds.ml index c964ecf1f..c964ecf1f 100644 --- a/intf/evar_kinds.ml +++ b/engine/evar_kinds.ml diff --git a/interp/interp.mllib b/interp/interp.mllib index bb22cf468..61313acc4 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,6 +1,7 @@ Tactypes Stdarg Genintern +Notation_term Notation_ops Notation Syntax_def diff --git a/intf/notation_term.ml b/interp/notation_term.ml index a9c2e2a53..a9c2e2a53 100644 --- a/intf/notation_term.ml +++ b/interp/notation_term.ml diff --git a/intf/intf.mllib b/intf/intf.mllib deleted file mode 100644 index 2b8960d3f..000000000 --- a/intf/intf.mllib +++ /dev/null @@ -1,11 +0,0 @@ -Constrexpr -Evar_kinds -Genredexpr -Locus -Extend -Notation_term -Decl_kinds -Glob_term -Misctypes -Pattern -Vernacexpr diff --git a/intf/decl_kinds.ml b/library/decl_kinds.ml index 0d3285311..0d3285311 100644 --- a/intf/decl_kinds.ml +++ b/library/decl_kinds.ml diff --git a/library/library.mllib b/library/library.mllib index e43bfb5a1..1c0368847 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -4,7 +4,9 @@ Libobject Summary Nametab Global +Decl_kinds Lib +Misctypes Declaremods Loadpath Library diff --git a/intf/misctypes.ml b/library/misctypes.ml index 72db3b31c..72db3b31c 100644 --- a/intf/misctypes.ml +++ b/library/misctypes.ml diff --git a/intf/constrexpr.ml b/pretyping/constrexpr.ml index fda31756a..fda31756a 100644 --- a/intf/constrexpr.ml +++ b/pretyping/constrexpr.ml diff --git a/intf/extend.ml b/pretyping/extend.ml index 734b859f6..734b859f6 100644 --- a/intf/extend.ml +++ b/pretyping/extend.ml diff --git a/intf/genredexpr.ml b/pretyping/genredexpr.ml index 80697461a..80697461a 100644 --- a/intf/genredexpr.ml +++ b/pretyping/genredexpr.ml diff --git a/intf/glob_term.ml b/pretyping/glob_term.ml index 84be15552..84be15552 100644 --- a/intf/glob_term.ml +++ b/pretyping/glob_term.ml diff --git a/intf/locus.ml b/pretyping/locus.ml index 95a2e495b..95a2e495b 100644 --- a/intf/locus.ml +++ b/pretyping/locus.ml diff --git a/intf/pattern.ml b/pretyping/pattern.ml index 76367b612..76367b612 100644 --- a/intf/pattern.ml +++ b/pretyping/pattern.ml diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index ae4ad0be7..d98026bc6 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,5 +1,5 @@ Geninterp -Ltac_pretype +Locus Locusops Pretype_errors Reductionops @@ -16,12 +16,19 @@ Evarsolve Recordops Evarconv Typing +Constrexpr +Genredexpr Miscops +Glob_term +Ltac_pretype Glob_ops Redops +Pattern Patternops Constr_matching Tacred +Extend +Vernacexpr Typeclasses_errors Typeclasses Classops diff --git a/intf/vernacexpr.ml b/pretyping/vernacexpr.ml index 4e1c986f1..4e1c986f1 100644 --- a/intf/vernacexpr.ml +++ b/pretyping/vernacexpr.ml |