diff --git a/Makefile b/Makefile
index 97020d9e..7c6e9395 100644
--- a/Makefile
+++ b/Makefile
@@ -75,8 +75,10 @@ endif
 #                    #
 ######################
 
-VFILES:= theories/Combi/combclass.v\
-  theories/Combi/ordtype.v\
+VFILES:= theories/Basic/combclass.v\
+  theories/Basic/congr.v\
+  theories/Basic/ordcast.v\
+  theories/Basic/ordtype.v\
   theories/Combi/partition.v\
   theories/Combi/permuted.v\
   theories/Combi/shape.v\
@@ -99,23 +101,21 @@ VFILES:= theories/Combi/combclass.v\
   theories/HookFormula/distr.v\
   theories/HookFormula/hook.v\
   theories/HookFormula/recyama.v\
-  theories/LRrule/congr.v\
+  theories/MPoly/antisym.v\
   theories/LRrule/extract.v\
   theories/LRrule/Greene_inv.v\
   theories/LRrule/Greene.v\
   theories/LRrule/implem.v\
-  theories/LRrule/ordcast.v\
   theories/LRrule/plactic.v\
   theories/LRrule/Schensted.v\
   theories/LRrule/Schur.v\
   theories/LRrule/shuffle.v\
-  theories/LRrule/sym_group.v\
   theories/LRrule/sympoly.v\
   theories/LRrule/stdplact.v\
   theories/LRrule/therule.v\
-  theories/LRrule/antisym.v\
   theories/LRrule/Schur_alt.v\
   theories/LRrule/Yam_plact.v\
+  theories/SymGroup/symgroup.v\
 
 -include $(addsuffix .d,$(VFILES))
 .SECONDARY: $(addsuffix .d,$(VFILES))
diff --git a/theories/Combi/combclass.v b/theories/Basic/combclass.v
similarity index 99%
rename from theories/Combi/combclass.v
rename to theories/Basic/combclass.v
index 6dd359bc..690202cf 100644
--- a/theories/Combi/combclass.v
+++ b/theories/Basic/combclass.v
@@ -1,4 +1,4 @@
-(** * Combi.Combi.combclass : Fintypes for Combinatorics *)
+(** * Combi.Basic.combclass : Fintypes for Combinatorics *)
 (******************************************************************************)
 (*     Copyright (C) 2014 2015 Florent Hivert <florent.hivert@lri.fr>         *)
 (*                                                                            *)
diff --git a/theories/LRrule/congr.v b/theories/Basic/congr.v
similarity index 99%
rename from theories/LRrule/congr.v
rename to theories/Basic/congr.v
index d61fcae6..91f58ab8 100644
--- a/theories/LRrule/congr.v
+++ b/theories/Basic/congr.v
@@ -1,3 +1,4 @@
+(** * Combi.Basic.congr : Rewriting rule and congruencies of words *)
 (******************************************************************************)
 (*       Copyright (C) 2014 Florent Hivert <florent.hivert@lri.fr>            *)
 (*                                                                            *)
diff --git a/theories/LRrule/ordcast.v b/theories/Basic/ordcast.v
similarity index 100%
rename from theories/LRrule/ordcast.v
rename to theories/Basic/ordcast.v
diff --git a/theories/Combi/ordtype.v b/theories/Basic/ordtype.v
similarity index 99%
rename from theories/Combi/ordtype.v
rename to theories/Basic/ordtype.v
index 84095bbe..8f86cab1 100644
--- a/theories/Combi/ordtype.v
+++ b/theories/Basic/ordtype.v
@@ -1,5 +1,4 @@
-(** * Combi.Combi.ordtype : Ordered Types *)
-
+(** * Combi.Basic.ordtype : Ordered Types *)
 (******************************************************************************)
 (*       Copyright (C) 2014 Florent Hivert <florent.hivert@lri.fr>            *)
 (*                                                                            *)
diff --git a/theories/LRrule/Schur_alt.v b/theories/LRrule/Schur_alt.v
index 753ed55d..28be296e 100644
--- a/theories/LRrule/Schur_alt.v
+++ b/theories/LRrule/Schur_alt.v
@@ -17,7 +17,7 @@ Require Import finset fintype finfun tuple bigop ssralg ssrint.
 Require Import fingroup perm.
 Require Import ssrcomplements poset freeg mpoly.
 Require Import tools ordtype sorted partition skewtab Schur therule.
-Require Import sym_group antisym.
+Require Import symgroup antisym.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/LRrule/sympoly.v b/theories/LRrule/sympoly.v
index eb1daa69..dafe18dd 100644
--- a/theories/LRrule/sympoly.v
+++ b/theories/LRrule/sympoly.v
@@ -16,7 +16,7 @@ Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path choice.
 Require Import finset fintype finfun tuple bigop ssralg ssrint.
 Require Import ssrcomplements poset freeg bigenough mpoly.
 
-Require Import partition skewtab Schur sym_group therule Schur_alt.
+Require Import partition skewtab Schur symgroup therule Schur_alt.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/LRrule/antisym.v b/theories/MPoly/antisym.v
similarity index 99%
rename from theories/LRrule/antisym.v
rename to theories/MPoly/antisym.v
index fc01ab31..8b858388 100644
--- a/theories/LRrule/antisym.v
+++ b/theories/MPoly/antisym.v
@@ -1,4 +1,4 @@
-(** * Combi.LRrule.antisym : Antisymmetric multivariate polynomials *)
+(** * Combi.MPoly.antisym : Antisymmetric multivariate polynomials *)
 (******************************************************************************)
 (*       Copyright (C) 2014 Florent Hivert <florent.hivert@lri.fr>            *)
 (*                                                                            *)
@@ -18,7 +18,7 @@ Require Import finset fintype finfun tuple bigop ssralg ssrint.
 Require Import fingroup perm zmodp binomial.
 Require Import ssrcomplements poset freeg mpoly.
 
-Require Import tools sym_group.
+Require Import tools symgroup.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/LRrule/sym_group.v b/theories/SymGroup/symgroup.v
similarity index 99%
rename from theories/LRrule/sym_group.v
rename to theories/SymGroup/symgroup.v
index c40850bf..cc277fb5 100644
--- a/theories/LRrule/sym_group.v
+++ b/theories/SymGroup/symgroup.v
@@ -1,4 +1,4 @@
-(** * Combi.LRrule.sym_group : The symmetric group *)
+(** * Combi.SymGroup.symgroup : The symmetric group *)
 (******************************************************************************)
 (*       Copyright (C) 2014 Florent Hivert <florent.hivert@lri.fr>            *)
 (*                                                                            *)