Rename Extraction to TemplateExtraction

Author: mattam82

extraction/Makefile

@@ -1,4 +1,4 @@
--R theories Extraction
+-R theories TemplateExtraction
 -Q ../template-coq/theories Template
 -I ../template-coq/src
 

extraction/_CoqProject

@@ -2,7 +2,7 @@
 
 From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
 From Template Require Import config utils monad_utils Ast univ Induction LiftSubst UnivSubst Typing Checker Retyping MetaTheory WcbvEval.
-From Extraction Require Ast Typing WcbvEval.
+From TemplateExtraction Require Ast Typing WcbvEval.
 Require Import String.
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
@@ -16,7 +16,7 @@ Definition is_prop_sort s :=
   | None => false
   end.
 
-Module E := Extraction.Ast.
+Module E := TemplateExtraction.Ast.
 
 Section Erase.
   Context `{F : Fuel}.
@@ -281,7 +281,7 @@ Fixpoint obs_eq (Σ : global_context) (v v' : term) (T : term) (s : universe) :
 
 Record extraction_post (Σ : global_context) (Σ' : Ast.global_context) (t : term) (t' : E.term) :=
   { extr_value : E.term;
-    extr_eval : Extraction.WcbvEval.eval (fst Σ') [] t' extr_value;
+    extr_eval : TemplateExtraction.WcbvEval.eval (fst Σ') [] t' extr_value;
     (* extr_equiv : obs_eq Σ v extr_value *) }.
 
 (** The extraction correctness theorem we conjecture. *)

extraction/theories/Extract.v

@@ -1,7 +1,7 @@
 (* Distributed under the terms of the MIT license.   *)
 
 From Template Require Import univ.
-From Extraction Require Import Ast.
+From TemplateExtraction Require Import Ast.
 Require Import List Program.
 Require Import BinPos.
 Require Import Coq.Arith.Compare_dec Bool.

extraction/theories/Induction.v

@@ -1,10 +1,7 @@
 (* Distributed under the terms of the MIT license.   *)
 
-Require Import List Program.
-Require Import Ast.
-Require Import BinPos.
-Require Import Coq.Arith.Compare_dec Bool.
-Require Import Induction.
+From Coq Require Import List Program BinPos Arith.Compare_dec Bool.
+From TemplateExtraction Require Import Ast Induction.
 
 (** * Lifting and substitution for the AST
 

extraction/theories/LiftSubst.v

@@ -2,7 +2,7 @@
 
 From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
 Require Import Template.config Template.utils Template.kernel.univ.
-From Extraction Require Import Ast Induction LiftSubst UnivSubst.
+From TemplateExtraction Require Import Ast Induction LiftSubst UnivSubst.
 Require Import String.
 Local Open Scope string_scope.
 Set Asymmetric Patterns.

extraction/theories/Typing.v

@@ -2,7 +2,7 @@
 
 From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
 From Template Require Import utils univ.
-From Extraction Require Import Ast Induction LiftSubst.
+From TemplateExtraction Require Import Ast Induction LiftSubst.
 From Template Require AstUtils.
 Require Import String.
 Local Open Scope string_scope.

extraction/theories/UnivSubst.v

@@ -2,7 +2,7 @@
 
 From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
 From Template Require Import config utils Ast univ.
-From Extraction Require Import Ast Induction LiftSubst UnivSubst Typing.
+From TemplateExtraction Require Import Ast Induction LiftSubst UnivSubst Typing.
 From Template Require AstUtils.
 Require Import String.
 Local Open Scope string_scope.