Revision 92900c9f4290d631543ddf717e369c3cfd96cc22 authored by Pierre-Yves Strub on 09 December 2015, 16:46:57 UTC, committed by Pierre-Yves Strub on 09 December 2015, 16:49:49 UTC
The mechanism is to forbid non-keyed matching in `rewrite` when LHS && RHS of the rewriting equation are convertible. Currently, the whole `rewrite` is rejected if the matching succeeds but the result would result in a identity rewriting. A better mechanism should embed the identity detection rewriting mechanism into the form matching one.
1 parent b3f11a9
pg-4.2.patch
diff -ru ProofGeneral-4.2.orig/Makefile ProofGeneral-4.2/Makefile
--- ProofGeneral-4.2.orig/Makefile 2012-03-05 19:52:34.000000000 +0100
+++ ProofGeneral-4.2/Makefile 2014-08-04 15:47:47.153429700 +0200
@@ -19,6 +19,8 @@
##
###########################################################################
+UNAME_S=$(shell uname -s)
+
# Set this according to your version of Emacs.
# NB: this is also used to set default install path names below.
EMACS=$(shell if [ -z "`which emacs`" ]; then echo "Emacs executable not found"; exit 1; else echo emacs; fi)
@@ -35,9 +37,13 @@
PREFIX=$(DESTDIR)/usr
DEST_PREFIX=$(DESTDIR)/usr
-PWD=$(shell pwd)
+PWD:=$(shell pwd)
+
+ifneq (,$(findstring CYGWIN,$(UNAME_S)))
+ PWD:=$(shell cygpath -m "$(PWD)")
+endif
-PROVERS=acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell
+PROVERS=acl2 ccc coq easycrypt hol98 isar lego hol-light phox pgshell pgocaml pghaskell
OTHER_ELISP=generic lib contrib/mmm
ELISP_DIRS=${PROVERS} ${OTHER_ELISP}
ELISP_EXTRAS=isar/interface isar/isartags
@@ -62,7 +68,7 @@
# only during compilation. Another idea: put a function in proof-site
# to output the compile-time load path and ELISP_DIRS so these are set
# just in that one place.
-BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (concat "${PWD}/" (symbol-name d))) (quote (${ELISP_DIRS}))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile
+BYTECOMP := $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (concat "$(PWD)/" (symbol-name d))) (quote (${ELISP_DIRS}))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile
EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done)
ELC=$(EL:.el=.elc)
Computing file changes ...