• Sylvain Dailler's avatar
    Fix subst as part of issue #16 · dc15aaf1
    Sylvain Dailler authored
    subst is now in three parts:
    - first it collects one equality per lsymbol that was given
    - it generates a list of tdecl which corresponds to the task minus
      the lsymbols and equalities collected before. It also substitutes all
      decls with these appropriate lsymbol erased.
    - it tries to add all this new tdecl into a new task with the safe
      Task.add_tdecl function. It tries to keep the order of decl as much as
      possible.
    
    There is room for improvement (in particular on efficiency of
    substitution).
    dc15aaf1
apply.ml 25.2 KB