diff --git a/src/ADTRefinement/FixedPoint.v b/src/ADTRefinement/FixedPoint.v
index 7a30da2d..b7a4a937 100644
--- a/src/ADTRefinement/FixedPoint.v
+++ b/src/ADTRefinement/FixedPoint.v
@@ -234,9 +234,9 @@ Definition cod_old_to_new {newRep oldRep fDom fCod}
 Proof.
   simpl; intros f.
   induction fDom; simpl in *.
-  exact { o : newRep * fCod |
+  exact ({ o : newRep * fCod |
           exists p,
-          computes_to f (p, snd o) /\ AbsR p (fst o)}.
+          computes_to f (p, snd o) /\ AbsR p (fst o)}).
   intro x.
   exact (IHfDom (f x)).
 Defined.
@@ -259,9 +259,9 @@ Definition cod_new_to_old {newRep oldRep fDom fCod}
 Proof.
   simpl; intros f.
   induction fDom; simpl in *.
-  exact { o : oldRep * fCod |
+  exact ({ o : oldRep * fCod |
           forall r_n',
-            computes_to f (r_n', snd o) -> AbsR (fst o) r_n'}.
+            computes_to f (r_n', snd o) -> AbsR (fst o) r_n'}).
   intro x.
   exact (IHfDom (f x)).
 Defined.
diff --git a/src/Common/SetEq.v b/src/Common/SetEq.v
index 60302868..66749f47 100644
--- a/src/Common/SetEq.v
+++ b/src/Common/SetEq.v
@@ -85,7 +85,7 @@ Lemma union_right :
     SetEq (SetUnion seq1 (x::seq2)) (x :: (SetUnion seq1 seq2)).
 Proof.
   intros; unfold SetEq, SetUnion; intuition;
-  repeat (rewrite in_app_iff in *; simpl in *);
+  repeat (rewrite in_app_iff in *; simpl in * );
   intuition.
 Qed.
 
diff --git a/src/Common/Tactics/CacheStringConstant.v b/src/Common/Tactics/CacheStringConstant.v
index f3a04480..ee19780f 100644
--- a/src/Common/Tactics/CacheStringConstant.v
+++ b/src/Common/Tactics/CacheStringConstant.v
@@ -7,7 +7,7 @@ Require Import
 Create HintDb stringCache.
 
 Ltac fold_string_hyps :=
-  (repeat foreach [ stringCache ] run (fun id => progress fold id in *)).
+  (repeat foreach [ stringCache ] run (fun id => progress fold id in * )).
 
 Ltac fold_string_hyps_in H :=
   repeat foreach [ stringCache ] run (fun id => progress fold id in H).
diff --git a/src/Computation/Refinements/Iterate_Decide_Comp.v b/src/Computation/Refinements/Iterate_Decide_Comp.v
index 1993cfbc..7304d302 100644
--- a/src/Computation/Refinements/Iterate_Decide_Comp.v
+++ b/src/Computation/Refinements/Iterate_Decide_Comp.v
@@ -100,7 +100,7 @@ Section Iterate_Decide_Comp.
                (if fin_eq_dec Ridx a then false else true) = true
                <-> a <> Ridx)
       as filter_dec'
-        by (intros; find_if_inside; try rewrite e; intuition; auto with *).
+        by (intros; find_if_inside; try rewrite e; intuition; auto with * ).
     split; intros.
     - eapply Iterate_Ensemble_equiv_filter'' with
       (filter := fun idx => idx <> Ridx)