Commits on Mar 19, 2020

1. [coq] Introduce Coq_scope …

   This PR is a RFC, as I'm not convinced at all this should be the way
   to go before we introduce handling of public Coq theories as to allow
   their inter-scope composition.
   
   The current approach to handling Coq theories ─ introduced in ocaml#2053 ─
   modified `Scope` and `Lib` adding a new library-like stanza type,
   `Coq_theory`.
   
   However, handling of libraries and theories is quite different so the
   above approach led to a few spurious code cases.
   
   There are two choices to improve this situation before we introduce
   `coq_public_libs`:
   
   - refactor `Scope` a bit more so we don't have to mess with
     `Lib.library_related_stanza`
   
     That's one option but still seems a bit invasive and messy for `scope.ml`.
   
   - split all Coq-related scope code to `Coq_scope` and handle things
     there. This is what this PR does.
   
   This approach does introduce some code duplication, so it is not clear
   if it is indeed a gain w.r.t. current status-quo.
   
   Code duplication could be solved by using some programming
   abstractions.
   
   Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

   

   ejgallego committed Mar 19, 2020
   Configuration menu

   • View commit details
   • Copy full SHA for aa359cb
   • Browse repository at this point

   Copy the full SHA

   aa359cb View commit details

   Browse the repository at this point in the history