coqide

patrick-nicodemus · Feb 26, 2019 · 96467c0 · 96467c0
1 parent 6f58b5a
commit 96467c0
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/INSTALL.md b/INSTALL.md
@@ -116,6 +116,8 @@ create HTML documentation.
    ```
    The path to that directory from here, by default, is ./sub/coq/user-contrib/.
 
+- To install [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html), see [INSTALL\_COQIDE](./INSTALL_COQIDE.md).
+
 ## TAGS files
 
 Emacs (which every UniMath user should become expert with) includes a facility

diff --git a/INSTALL_COQIDE.md b/INSTALL_COQIDE.md
@@ -16,5 +16,6 @@ Later on, after running the command `make install` as instructed below, in
 order to run the program ```coqide```, you may use the following command.
 
 ```bash
-$ sub/coq/bin/coqide -indices-matter -type-in-type -Q UniMath UniMath
+$ sub/coq/bin/coqide <flags>
 ```
+where `<flags>` are the options passed to `coq` as per the [Emacs configuration file](./UniMath/.dir-locals.el).