added installaation instructions

README.md

@@ -2,6 +2,15 @@
 
 An implementation of Separation Logic for a monadic language, while while loops defined using domain theory.
 
+Developed in Coq 8.19.1. 
+
+Uses the AAC package for associative-commutative rewriting.
+
+Installation instructions for Coq: https://coq.inria.fr/opam-using.html
+
+Installation instructions for the AAC package : https://github.com/coq-community/aac-tactics
+
+
 ## Files:
 
 - ACPO.v, ADCPO.v, CPO.v, EXP.v, FunComp.v, Haddock.v, Ideal.v, Kleene.v, Option.v, Setof.v : domain-theoretical constructions.