.dir-locals.el

((coq-mode
  . ((eval . 
	   (let* ((Workshops-topdir (expand-file-name (locate-dominating-file buffer-file-name ".dir-locals.el")))
		  (unimath-topdir (concat Workshops-topdir "UniMath/")))
	     (setq fill-column 100)
	     (make-local-variable 'coq-use-project-file)
	     (setq coq-use-project-file nil)
	     (make-local-variable 'coq-prog-args)
	     (setq coq-prog-args `("-emacs" "-noinit" "-indices-matter" "-type-in-type"
				   "-w" "-notation-overridden,-local-declaration,+uniform-inheritance,-deprecated-option"
				   "-Q" ,(concat unimath-topdir "UniMath") "UniMath"
				   "-R" "." "Top"
				   ))
	     (make-local-variable 'coq-prog-name)
	     (setq coq-prog-name (concat unimath-topdir "sub/coq/bin/coqtop"))
	     (make-local-variable 'before-save-hook)
	     (add-hook 'before-save-hook 'delete-trailing-whitespace)
	     (modify-syntax-entry ?' "w")
	     (modify-syntax-entry ?_ "w")
	     (if (not (memq 'agda-input features))
		 (load (concat unimath-topdir "emacs/agda/agda-input")))
	     (if (not (member '("chimney" "╝") agda-input-user-translations))
		 (progn
		   (setq agda-input-user-translations (cons '("chimney" "╝") agda-input-user-translations))
		   (setq agda-input-user-translations (cons '("==>" "⟹") agda-input-user-translations))
		   (agda-input-setup)))
	     (set-input-method "Agda"))))))