Skip to main content

Browse the archive

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 
Crude detection of identity rewriting.
 
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
Raw File
proof-site.patch 
--- proof-site.el.orig	2013-03-27 12:42:07.061084211 +0100
+++ proof-site.el	2013-03-27 12:41:51.080922301 +0100
@@ -40,6 +40,7 @@
       (isar "Isabelle" "thy")
       (coq "Coq" "v" nil (".vo" ".glob"))
       (phox "PhoX" "phx")
+      (easycrypt "EasyCrypt" "ec" ".*\\.eca?")
 
       ;; Obscure instances or conflict with other Emacs modes.
back to top