package coq-core
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
  The Coq Proof Assistant -- Core Binaries and Tools
Install
    
    dune-project
 Dependency
Authors
Maintainers
Sources
  
    
      coq-8.18.0.tar.gz
    
    
        
    
  
  
  
    
  
  
    
  
        md5=8d852367b54f095d9fbabd000304d450
    
    
  sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
    
    
  doc/coq-core.engine/Proofview_monad/Trace/index.html
Module Proofview_monad.TraceSource
The intent is that an 'a forest is a list of messages of type 'a. But messages can stand for a list of more precise messages, hence the structure is organised as a tree.
To build a trace incrementally, we use an intermediary data structure on which we can define an S-expression like language (like a simplified xml except the closing tags do not carry a name).
close closes the last open tag. It is the responsibility of the user to close all the tags.
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >