Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 344a4789 authored by Sylvain Dailler's avatar Sylvain Dailler

Revert "disabled Isabelle realizations of set.Set and set.FSet"

This reverts commit fb4cb734.
parent fb4cb734
......@@ -1273,9 +1273,8 @@ ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/r
ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/number/, $(ISABELLELIBS_NUMBER_FILES)))
# broken
# ISABELLELIBS_SET_FILES = Set Fset
# ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/set/, $(ISABELLELIBS_SET_FILES)))
ISABELLELIBS_SET_FILES = Set Fset
ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/set/, $(ISABELLELIBS_SET_FILES)))
ISABELLELIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/map/, $(ISABELLELIBS_MAP_FILES)))
......@@ -1300,8 +1299,8 @@ drivers/isabelle-realizations.aux: Makefile
echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_NUMBER_FILES); do \
echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
# for f in $(ISABELLELIBS_SET_FILES); do \
# echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_SET_FILES); do \
echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_MAP_FILES); do \
echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_LIST_FILES); do \
......
theory Why3
imports
Why3_Map
(* broken Why3_Set *)
Why3_Set
Why3_List
Why3_Int
Why3_Bool
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment