1. 04 Sep, 2014 13 commits
  2. 03 Sep, 2014 7 commits
  3. 02 Sep, 2014 13 commits
  4. 01 Sep, 2014 7 commits
    • MARCHE Claude's avatar
      prepare for opam package · dc0d5af2
      MARCHE Claude authored
      dc0d5af2
    • MARCHE Claude's avatar
      22b782f6
    • MARCHE Claude's avatar
      replace use of bisect by efficient provers · 3a2f6130
      MARCHE Claude authored
      3a2f6130
    • Andrei Paskevich's avatar
      fix #17137 · 573870e0
      Andrei Paskevich authored
      Currently, clones "ts -> ty" are represented as "ts -> ts[=ty]",
      where the second type symbol is an alias created on the fly
      for the desired type. The problem comes when we want to clone
      a theory that contains such a cloning declaration. Since these
      aliases are "non-citizens" -- they are not properly declared,
      they are not put in the known_map, and they are not listed as
      locally declared symbols of the theory -- cloning of the cloning
      declaration mistakes them for external symbols and ignores them.
      Thus, the aliased type goes into the cloned theory as is, which
      provokes the error.
      
      The fix consists in an additional test for non-local type symbols.
      If such a symbol is an alias for a type that is actually cloneable,
      we conclude that the symbol is not external, but is a mere proxy
      for the aliased type, and so we clone the type and create a fresh
      type alias for it.
      
      A proper fix would be to always clone type symbols into types and
      never introduce the proxy type aliases. This is a more intrusive
      change, however, so let's start with a bandage.
      573870e0
    • MARCHE Claude's avatar
      updated ROADMAP · 09d37ec0
      MARCHE Claude authored
      09d37ec0
    • MARCHE Claude's avatar
      3db9da11
    • MARCHE Claude's avatar
      Fixed unproved sessions · f1153ff6
      MARCHE Claude authored
      f1153ff6