removed devcomments

imdea-software · Sep 23, 2024 · 7ecce21 · 7ecce21
1 parent ae6f24f
commit 7ecce21
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 20 deletions.
diff --git a/examples/hashtab.v b/examples/hashtab.v
@@ -22,9 +22,6 @@ From htt Require Import array kvmaps.
 (* hash table is array of buckets, i.e. KV maps *)
 (* bucket indices are provided by the hash function *)
 (* using dynaming kv-maps for buckets *)
-(* DEVCOMMENT: *)
-(*  it's possible to develop this with static buckers *)
-(* /DEVCOMMENT *)
 
 Module Type Hashtab_sig.
 Parameter root : forall {K : ordType} {V : Type} (buckets : dkvm K V)

diff --git a/htt/domain.v b/htt/domain.v
@@ -1028,10 +1028,4 @@ HB.instance Definition _ :=
   isContFun.Build (S1*S2)%type (T1*T2)%type (f1 \* f2) prod_is_cont.
 End ProdCont.
 
-(* DEVCOMMENT *)
-(* TODO: *)
-(* 1. limit of a chain of continuous functions is a continuous function *)
-(* 2. CPO of continuous functions should be the subCPO of functions *)
-(* 3. kleene_lfp is a continuous operation *)
-(* /DEVCOMMENT *)
 
diff --git a/htt/dune b/htt/dune