Better use of tables for storing results of extract_ind (bug #1709)

 It is critical to avoid duplicated calls to extract_ind (see e.g. 
 example in #1709). But the same kernel_name can lead to different 
 inductive bodies, due to module substitutions. So we used to 
 factorize only "visible" kn, that were not subject to change under 
 substitution. As shown by P. Cregut in #1709, this is not enough. 
 New approach is now to store also Coq inductive data (mib). If the 
 recorded mib matches the current one, we trust the recorded result, 
 otherwise we start a fresh computation of extract_ind. 



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10194 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions