Skip to main content

Browse the archive

Revision 1b9269a0fcb1147c4dc6eb9f31bd4a02290ba783 authored by Pierre-Yves Strub on 21 May 2018, 20:36:27 UTC, committed by Pierre-Yves Strub on 21 May 2018, 20:36:27 UTC 
New tactic: 'conseq ?>' where '?>' is a crush mode.
 
Simplifies *HL post-condition from the pre using
a crush-like simplication.

Co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr>
1 parent 165ee99
Raw File
Makefile.system 
# -*- Makefile -*-

# --------------------------------------------------------------------
OCAML    := $(shell ocamlbuild -which ocamlc 2>/dev/null || echo false)
CC       := gcc
MACHINE  := $(shell $(OCAML) -ccopt -dumpmachine dummy.c 2>/dev/null)
UNAME    := $(shell uname -s)
EXE      :=

ifneq (,$(findstring CYGWIN,$(UNAME)))
  CC = $(MACHINE)-gcc
endif

ifneq (,$(findstring mingw,$(MACHINE)))
EXE := .exe
endif

ifneq (,$(findstring cygwin,$(MACHINE)))
EXE := .exe
endif
back to top