fix the make autosubst target

Author: kyoDralliam

Makefile

@@ -3,7 +3,7 @@
 all: partial-fun logrel
 
 autosubst:
-	autosubst -f -s ucoq -v ge813 -p ./theories/AutoSubst/Ast_preamble -no-static -o ./theories/AutoSubst/Ast.v ./theories/AutoSubst/Ast.sig
+	autosubst -f -s urocq -v ge813 -p ./theories/AutoSubst/Ast_preamble -no-static -o ./theories/AutoSubst/Ast.v ./theories/AutoSubst/Ast.sig
 partial-fun:
 	@+$(MAKE) -C coq-partialfun all
 

theories/AutoSubst/Ast.v

@@ -131,7 +131,8 @@ Lemma congr_tId {s0 : term} {s1 : term} {s2 : term} {t0 : term} {t1 : term}
 Proof.
 exact (eq_trans
          (eq_trans (eq_trans eq_refl (ap (fun x => tId x s1 s2) H0))
-            (ap (fun x => tId t0 x s2) H1)) (ap (fun x => tId t0 t1 x) H2)).
+            (ap (fun x => tId t0 x s2) H1))
+         (ap (fun x => tId t0 t1 x) H2)).
 Qed.
 
 Lemma congr_tRefl {s0 : term} {s1 : term} {t0 : term} {t1 : term}
@@ -588,15 +589,17 @@ subst_term tau_term (ren_term xi_term s) = subst_term theta_term s :=
       congr_tNatElim
         (compRenSubst_term (upRen_term_term xi_term) (up_term_term tau_term)
            (up_term_term theta_term) (up_ren_subst_term_term _ _ _ Eq_term)
-           s0) (compRenSubst_term xi_term tau_term theta_term Eq_term s1)
+           s0)
+        (compRenSubst_term xi_term tau_term theta_term Eq_term s1)
         (compRenSubst_term xi_term tau_term theta_term Eq_term s2)
         (compRenSubst_term xi_term tau_term theta_term Eq_term s3)
   | tEmpty => congr_tEmpty
   | tEmptyElim s0 s1 =>
       congr_tEmptyElim
         (compRenSubst_term (upRen_term_term xi_term) (up_term_term tau_term)
            (up_term_term theta_term) (up_ren_subst_term_term _ _ _ Eq_term)
-           s0) (compRenSubst_term xi_term tau_term theta_term Eq_term s1)
+           s0)
+        (compRenSubst_term xi_term tau_term theta_term Eq_term s1)
   | tSig s0 s1 =>
       congr_tSig (compRenSubst_term xi_term tau_term theta_term Eq_term s0)
         (compRenSubst_term (upRen_term_term xi_term) (up_term_term tau_term)
@@ -606,7 +609,8 @@ subst_term tau_term (ren_term xi_term s) = subst_term theta_term s :=
       congr_tPair (compRenSubst_term xi_term tau_term theta_term Eq_term s0)
         (compRenSubst_term (upRen_term_term xi_term) (up_term_term tau_term)
            (up_term_term theta_term) (up_ren_subst_term_term _ _ _ Eq_term)
-           s1) (compRenSubst_term xi_term tau_term theta_term Eq_term s2)
+           s1)
+        (compRenSubst_term xi_term tau_term theta_term Eq_term s2)
         (compRenSubst_term xi_term tau_term theta_term Eq_term s3)
   | tFst s0 =>
       congr_tFst (compRenSubst_term xi_term tau_term theta_term Eq_term s0)
@@ -627,7 +631,8 @@ subst_term tau_term (ren_term xi_term s) = subst_term theta_term s :=
            (up_term_term (up_term_term tau_term))
            (up_term_term (up_term_term theta_term))
            (up_ren_subst_term_term _ _ _
-              (up_ren_subst_term_term _ _ _ Eq_term)) s2)
+              (up_ren_subst_term_term _ _ _ Eq_term))
+           s2)
         (compRenSubst_term xi_term tau_term theta_term Eq_term s3)
         (compRenSubst_term xi_term tau_term theta_term Eq_term s4)
         (compRenSubst_term xi_term tau_term theta_term Eq_term s5)
@@ -736,7 +741,8 @@ ren_term zeta_term (subst_term sigma_term s) = subst_term theta_term s :=
            (upRen_term_term (upRen_term_term zeta_term))
            (up_term_term (up_term_term theta_term))
            (up_subst_ren_term_term _ _ _
-              (up_subst_ren_term_term _ _ _ Eq_term)) s2)
+              (up_subst_ren_term_term _ _ _ Eq_term))
+           s2)
         (compSubstRen_term sigma_term zeta_term theta_term Eq_term s3)
         (compSubstRen_term sigma_term zeta_term theta_term Eq_term s4)
         (compSubstRen_term sigma_term zeta_term theta_term Eq_term s5)
@@ -760,7 +766,8 @@ exact (fun n =>
                 (eq_sym
                    (compSubstRen_term tau_term shift
                       (funcomp (ren_term shift) tau_term) (fun x => eq_refl)
-                      (sigma n'))) (ap (ren_term shift) (Eq n')))
+                      (sigma n')))
+                (ap (ren_term shift) (Eq n')))
        | O => eq_refl
        end).
 Qed.
@@ -847,7 +854,8 @@ subst_term tau_term (subst_term sigma_term s) = subst_term theta_term s :=
            (up_term_term (up_term_term tau_term))
            (up_term_term (up_term_term theta_term))
            (up_subst_subst_term_term _ _ _
-              (up_subst_subst_term_term _ _ _ Eq_term)) s2)
+              (up_subst_subst_term_term _ _ _ Eq_term))
+           s2)
         (compSubstSubst_term sigma_term tau_term theta_term Eq_term s3)
         (compSubstSubst_term sigma_term tau_term theta_term Eq_term s4)
         (compSubstSubst_term sigma_term tau_term theta_term Eq_term s5)
@@ -989,7 +997,8 @@ Fixpoint rinst_inst_term (xi_term : nat -> nat) (sigma_term : nat -> term)
         (rinst_inst_term (upRen_term_term (upRen_term_term xi_term))
            (up_term_term (up_term_term sigma_term))
            (rinstInst_up_term_term _ _ (rinstInst_up_term_term _ _ Eq_term))
-           s2) (rinst_inst_term xi_term sigma_term Eq_term s3)
+           s2)
+        (rinst_inst_term xi_term sigma_term Eq_term s3)
         (rinst_inst_term xi_term sigma_term Eq_term s4)
         (rinst_inst_term xi_term sigma_term Eq_term s5)
   end.
@@ -1156,7 +1165,8 @@ Ltac asimpl := check_no_evars;
                 repeat
                  unfold VarInstance_term, Var, ids, Ren_term, Ren1, ren1,
                   Up_term_term, Up_term, up_term, Subst_term, Subst1, subst1
-                  in *; asimpl'; minimize.
+                  in *;
+                asimpl'; minimize.
 
 Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.
 

theories/AutoSubst/Ast_preamble

@@ -1,5 +1,7 @@
+(** * LogRel.AutoSubst.Ast: abstract syntax tree, definitions of renamings, substitutions and many lemmas, generated using AutoSubst. *)
+
 From LogRel.AutoSubst Require Import core unscoped.
 From LogRel.Syntax Require Import BasicAst.
-From Coq Require Import Setoid Morphisms Relation_Definitions.
+From Stdlib Require Import Setoid Morphisms Relation_Definitions.