script

(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(**********************************************************************)
(*               Typed LambdaFactor Calculus                          *)
(*                                                                    *)
(* is implemented in Coq by adapting the implementation of            *) 
(* Lambda Calculus  from Project Coq                                  *)
(* 2015                                                               *)
(**********************************************************************)

(**********************************************************************)
(*                       script                                       *)
(*                                                                    *)
(*                     Barry Jay                                      *)
(*                                                                    *)
(**********************************************************************)

coqc General;
coqc Test; 
coqc LamSF_Terms.v;
coqc LamSF_Tactics.v 
coqc LamSF_Substitution_term.v; 

coqc Components.v;
coqc Compounds.v;
coqc LamSF_reduction.v; 
coqc LamSF_Normal.v;  
coqc LamSF_Closed.v;  
coqc LamSF_Eval.v;   

coqc Beta_Reduction.v;
coqc LamSF_Redexes.v;
coqc LamSF_Substitution.v;
coqc LamSF_Residuals.v;
coqc LamSF_Marks.v;
coqc LamSF_Simulation.v;
coqc LamSF_Cube.v;
coqc LamSF_Confluence.v;

coqc type_derivation
coqc type_derivation_resi
coqc type_derivation_rwf
coqc operator_types
coqc subject_reduction

coqc Equal.v; 
coqc Unstar
coqc Slow_quote; 
coqc Unquote;