• Sylvain Dailler's avatar
    In ce collection pass, constants can now have several projections. · da3f5499
    Sylvain Dailler authored
    These projections are necessary because records have changed from
    old system to new system. Previously, a record was never abstract.
    Subsequently, we could always give value to its fields independently.
    Now, when a record (or algebraic type, not handled by this commit) is
    abstract, we use the function defined for its fields as projections.
    So, we need to have several projections per constant in order to represent
    those as values.
    
    This patch is also a first step to the necessary cleaning of ce treatment
    code.
    da3f5499
call_provers.ml 17.8 KB