Make Clight independent of CompCert C.

Common parts are factored out in cfrontend/Ctypes.v and cfrontend/Cop.v


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2060 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 8 insertions, 7 deletions

diff --git a/LICENSE b/LICENSE
index 42c4b152..a6155925 100644
--- a/LICENSE
+++ b/LICENSE
@@ -22,13 +22,14 @@ option) any later version:
     backend/CMtypecheck.ml           common/Mem.v         
     backend/CMtypecheck.mli          common/Smallstep.v   
     cfrontend/C2C.ml                 common/Switch.v      
-    cfrontend/Csem.v                 common/Values.v      
-    cfrontend/Csyntax.v              lib/Coqlib.v         
-    cfrontend/Cstrategy.v            lib/Floats.v         
-    cfrontend/Clight.v               lib/Integers.v       
-    cfrontend/PrintCsyntax.ml        lib/Maps.v           
-    cfrontend/PrintClight.ml         lib/Parmov.v         
-                                     lib/Camlcoq.ml       
+    cfrontend/Cop.v                  common/Values.v      
+    cfrontend/Ctypes.v               lib/Coqlib.v         
+    cfrontend/Csem.v                 lib/Floats.v         
+    cfrontend/Csyntax.v              lib/Integers.v       
+    cfrontend/Cstrategy.v            lib/Maps.v           
+    cfrontend/Clight.v               lib/Parmov.v         
+    cfrontend/PrintCsyntax.ml        lib/Camlcoq.ml       
+    cfrontend/PrintClight.ml         
 
     all files in the runtime/ directory
     all files in the cparser/ directory