1. 12 Feb, 2019 2 commits
  2. 11 Feb, 2019 1 commit
  3. 04 Dec, 2018 1 commit
  4. 13 Nov, 2018 1 commit
  5. 30 Oct, 2018 1 commit
  6. 29 Oct, 2018 1 commit
  7. 23 Oct, 2018 1 commit
  8. 02 Oct, 2018 1 commit
  9. 24 Sep, 2018 1 commit
  10. 20 Sep, 2018 1 commit
  11. 01 Jun, 2018 3 commits
  12. 14 May, 2018 1 commit
  13. 09 May, 2018 1 commit
  14. 22 Mar, 2018 1 commit
    • Raphael Rieu-Helft's avatar
      Add a transformation to rewrite several equalities at once · fc53feba
      Raphael Rieu-Helft authored
      When many equalities have to be rewritten, using the existing rewrite transformation repeatedly wastes a lot of time in declaration and task construction.
      The rewrite_list transformation rewrites all equalities first and then builds the new declarations and tasks only once.
      fc53feba
  15. 07 Feb, 2018 1 commit
  16. 24 Jan, 2018 1 commit
    • Sylvain Dailler's avatar
      Fix issue #79 · d8017e38
      Sylvain Dailler authored
      For first_order_matching, adding a bound_vars set to disallow substitution
      by terms containing bounded vars.
      d8017e38
  17. 22 Jan, 2018 1 commit
    • 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
  18. 12 Jan, 2018 1 commit
  19. 15 Nov, 2017 1 commit
    • Sylvain Dailler's avatar
      fixes #19 · 3c006d28
      Sylvain Dailler authored
      Merged apply and apply_with (resp. rewrite and rewrite_with). Typo in
      error returned by apply. Also adding session for 19.
      3c006d28
  20. 14 Nov, 2017 1 commit
    • Sylvain Dailler's avatar
      fixes #19 · 35418b73
      Sylvain Dailler authored
      Adding a new tactic apply_with which allows to give an ordered list of
      terms to instantiate variables that are not found by apply. Same for
      rewrite with rewrite_with. These tactics will be merged with apply/rewrite
      when detached are implemented. This needs to be tested extensively.
      Also, print terms with their types in errors.
      35418b73
  21. 08 Nov, 2017 2 commits
  22. 18 Oct, 2017 1 commit
  23. 13 Oct, 2017 1 commit
  24. 26 Sep, 2017 1 commit
  25. 24 Sep, 2017 1 commit
  26. 02 Aug, 2017 1 commit
  27. 01 Aug, 2017 1 commit
  28. 06 Jul, 2017 1 commit
  29. 05 Jul, 2017 1 commit
    • MARCHE Claude's avatar
      ITP: support for qualified ident and infix ident · bccdfacc
      MARCHE Claude authored
      command "search" and transformations taking idents as arguments now can
      support qualified idents and infix symbols.
      
      For example, "search (+) (*)" returns the distributivity axioms
      
      FIXME: "search Int.(+)" fails, probably missing namespaced for
      imported modules
      bccdfacc
  30. 04 Jul, 2017 1 commit
  31. 29 Jun, 2017 1 commit