package coq
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
  Formal proof management system
Install
    
    dune-project
 Dependency
Authors
Maintainers
Sources
  
    
      coq-8.15.2.tar.gz
    
    
        
    
  
  
  
    
  
        sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926
    
    
  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)"
  >