Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

  1. 21 Dec, 2017 3 commits
    • MARCHE Claude's avatar
      test file for issue #60 · db728258
      MARCHE Claude authored
    • MARCHE Claude's avatar
      Merge branch 'new_ide' · b6e25241
      MARCHE Claude authored
      # Conflicts:
      #	examples/residual/why3session.xml
      #	examples/residual/why3shapes.gz
      #	lib/coq/int/Int.v
      #	lib/coq/int/NumOf.v
      #	lib/coq/map/Const.v
      #	lib/coq/map/Map.v
      #	lib/coq/map/MapInjection.v
      #	lib/coq/map/MapPermut.v
      #	lib/coq/map/Occ.v
      #	lib/coq/number/Divisibility.v
      #	lib/coq/real/Real.v
      #	lib/coq/set/Set.v
    • MARCHE Claude's avatar
      fix issue #61 · 50317a3a
      MARCHE Claude authored
      proof nodes are not anymore marked obsolete when they are detached
  2. 20 Dec, 2017 2 commits
  3. 19 Dec, 2017 4 commits
    • Sylvain Dailler's avatar
      Fixes #58 · 373a7bc9
      Sylvain Dailler authored
      Remove now selects the parent of the removed node when a selected node is
      contained in the removed subtree.
      Adding a function that check a request is not referring to obsolete
      node_id in If such a request is found, the error that owuld
      have been generated is not sent to the ide.
    • Sylvain Dailler's avatar
    • Mário Pereira's avatar
    • Sylvain Dailler's avatar
      Fixes #59 · 3fce61d8
      Sylvain Dailler authored
      Adding random (to be set) shortcut to the functions: next unproven goal,
      expand, expand_all, collapse, parent, first_child. These can be accessed
      from the command line by typing the command (list_ide_command is for help
      on these commands).
      Fixing shortcuts with ~key instead of add_accelerator.
      [get_first_unproven_goal_around cn] now returns a different node from cn
      and, if a brother of cn is returned, it returns preferably one placed
      after cn in the tree.
  4. 16 Dec, 2017 1 commit
    • Mário Pereira's avatar
      Extraction of range types: · 2f5afda0
      Mário Pereira authored
      - even for range types fitting 31-bit signed integers the user must provide a
      driver in order to get them extracted to OCaml's type 'int'
  5. 15 Dec, 2017 7 commits
  6. 14 Dec, 2017 13 commits
  7. 13 Dec, 2017 7 commits
  8. 12 Dec, 2017 3 commits