Merge branch 'SymGroup'

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))

theories/Combi/combclass.v → 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 <[email protected]>         *)
 (*                                                                            *)

theories/LRrule/congr.v → theories/Basic/congr.v

@@ -1,3 +1,4 @@
+(** * Combi.Basic.congr : Rewriting rule and congruencies of words *)
 (******************************************************************************)
 (*       Copyright (C) 2014 Florent Hivert <[email protected]>            *)
 (*                                                                            *)

theories/Combi/ordtype.v → theories/Basic/ordtype.v

@@ -1,5 +1,4 @@
-(** * Combi.Combi.ordtype : Ordered Types *)
-
+(** * Combi.Basic.ordtype : Ordered Types *)
 (******************************************************************************)
 (*       Copyright (C) 2014 Florent Hivert <[email protected]>            *)
 (*                                                                            *)

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.

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.

theories/LRrule/antisym.v → 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 <[email protected]>            *)
 (*                                                                            *)
@@ -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.

theories/LRrule/sym_group.v → 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 <[email protected]>            *)
 (*                                                                            *)