Porting to Coq 8.7

.depend

@@ -1,7 +1,7 @@
 AbsSNT.vo AbsSNT.glob AbsSNT.v.beautified: AbsSNT.v GenLemmas.vo AbsTheoryIntp.vo
 AbsTheoryIntp.vo AbsTheoryIntp.glob AbsTheoryIntp.v.beautified: AbsTheoryIntp.v GenLemmas.vo AbsTheorySyn.vo AbsTheorySem.vo
 AbsTheorySem.vo AbsTheorySem.glob AbsTheorySem.v.beautified: AbsTheorySem.v GenLemmas.vo
-AbsTheorySyn.vo AbsTheorySyn.glob AbsTheorySyn.v.beautified: AbsTheorySyn.v
+AbsTheorySyn.vo AbsTheorySyn.glob AbsTheorySyn.v.beautified: AbsTheorySyn.v CoqCompat.vo
 CCTnat.vo CCTnat.glob CCTnat.v.beautified: CCTnat.v Explicit_sub.vo FOTheory.vo basic.vo
 CCUT.vo CCUT.glob CCUT.v.beautified: CCUT.v Models.vo GenModelSN.vo ZF.vo ZFind_nat.vo SN_CC.vo
 Can.vo Can.glob Can.v.beautified: Can.v Lambda.vo
@@ -46,8 +46,8 @@ ModelZF.vo ModelZF.glob ModelZF.v.beautified: ModelZF.v basic.vo Sublogic.vo Mod
 Model_variance.vo Model_variance.glob Model_variance.v.beautified: Model_variance.v ZF.vo ZFcoc.vo ZFfunext.vo ModelZF.vo
 Models.vo Models.glob Models.v.beautified: Models.v basic.vo
 MyList.vo MyList.glob MyList.v.beautified: MyList.v
-Nest.vo Nest.glob Nest.v.beautified: Nest.v
-NonUniform.vo NonUniform.glob NonUniform.v.beautified: NonUniform.v
+Nest.vo Nest.glob Nest.v.beautified: Nest.v CoqCompat.vo
+NonUniform.vo NonUniform.glob NonUniform.v.beautified: NonUniform.v CoqCompat.vo
 ObjectSN.vo ObjectSN.glob ObjectSN.v.beautified: ObjectSN.v basic.vo Models.vo VarMap.vo Lambda.vo
 ObjectSN2.vo ObjectSN2.glob ObjectSN2.v.beautified: ObjectSN2.v basic.vo Models.vo VarMap.vo Lambda.vo
 PIntp.vo PIntp.glob PIntp.v.beautified: PIntp.v GenLemmas.vo AbsTheoryIntp.vo PSyn.vo PSem.vo
@@ -76,7 +76,7 @@ Sat.vo Sat.glob Sat.v.beautified: Sat.v Lambda.vo Can.vo
 SnModels.vo SnModels.glob SnModels.v.beautified: SnModels.v basic.vo Models.vo Sat.vo
 StrengthenECC.vo StrengthenECC.glob StrengthenECC.v.beautified: StrengthenECC.v TypeECC.vo
 Sublogic.vo Sublogic.glob Sublogic.v.beautified: Sublogic.v basic.vo Logics.vo
-Term.vo Term.glob Term.v.beautified: Term.v
+Term.vo Term.glob Term.v.beautified: Term.v CoqCompat.vo
 TermECC.vo TermECC.glob TermECC.v.beautified: TermECC.v
 TheoryInTerm.vo TheoryInTerm.glob TheoryInTerm.v.beautified: TheoryInTerm.v ZFtheory.vo GenModel.vo ZFcoc.vo ModelZF.vo
 TypModels.vo TypModels.glob TypModels.v.beautified: TypModels.v Models.vo
@@ -141,5 +141,7 @@ ZFuniv.vo ZFuniv.glob ZFuniv.v.beautified: ZFuniv.v Sat.vo ZF.vo ZFcoc.vo ZFord.
 ZFuniv_real.vo ZFuniv_real.glob ZFuniv_real.v.beautified: ZFuniv_real.v Sat.vo ZF.vo ZFcoc.vo ZFord.vo ZFgrothendieck.vo ZFlambda.vo Models.vo SnModels.vo
 ZFwf.vo ZFwf.glob ZFwf.v.beautified: ZFwf.v basic.vo ZF.vo ZFrepl.vo ZFpairs.vo ZFrelations.vo
 ZFwpaths.vo ZFwpaths.glob ZFwpaths.v.beautified: ZFwpaths.v ZF.vo ZFpairs.vo ZFsum.vo ZFnats.vo ZFrelations.vo ZFtarski.vo ZFstable.vo ZFgrothendieck.vo ZFlist.vo
-basic.vo basic.glob basic.v.beautified: basic.v
+CoqCompat.vo CoqCompat.glob CoqCompat.v.beautified: CoqCompat.v
+basic.vo basic.glob basic.v.beautified: basic.v CoqCompat.vo
 test.vo test.glob test.v.beautified: test.v Lambda.vo
+hEns.vo hEns.global hEns.v.beautified: hEns.v ZFskol.vo Sublogic.vo

AbsTheorySyn.v

@@ -1,5 +1,5 @@
 Require Import List.
-Require Import Omega.
+Require Export CoqCompat.
 
 (******************************************************************************************)
 (******************************************************************************************)

CoqCompat.v

@@ -0,0 +1,11 @@
+Require Export Coq85.
+Require Export AdmitAxiom.
+
+Require Coq.omega.Omega.
+Ltac omega := Coq.omega.Omega.omega.
+Global Set Asymmetric Patterns.
+
+Require Import Morphisms.
+Existing Instance respectful_per.
+
+Notation value := Some.

Ens.v

@@ -813,7 +813,7 @@ Fixpoint V (x:set) := union (replf x (fun x' => power (V x'))).
 
 Lemma V_morph : forall x x', eq_set x x' -> eq_set (V x) (V x').
 induction x; destruct x'; intros.
-simpl V; unfold replf; simpl sup.
+simpl V; unfold replf.
 apply union_morph.
 simpl in H0.
 destruct H0.
@@ -1105,7 +1105,7 @@ assert (Pwit : forall x, x ∈ A -> exists y, P x (V y)).
  apply V_sub with (V x0).
   apply V_mono; exists tt; apply eq_set_refl.
   apply V_intro.
-destruct (@repl_ax A (fun x y => lst_rk (P x) y)); eauto using lst_fun, lst_ex.
+destruct (@repl_ax A (fun x y => lst_rk (P x) y)); simpl; eauto using lst_fun, lst_ex.
  intros.
  apply lst_rk_morph with (P x) y; trivial.
  intros.
@@ -1263,7 +1263,7 @@ generalize (H (sup bool (fun b => if b then empty else singl empty))
               (sup bool (fun b => if b then singl empty else empty))).
 simpl; intros.
 assert (singl empty == empty).
- refine (let H1 := H0 _ in _).
+ simple refine ((fun H1 => _) (H0 _)); swap 1 2.
   split; intros.
    exists (negb i).
    destruct i; apply eq_set_refl.

EnsEm.v

@@ -1115,7 +1115,7 @@ Fixpoint V (x:set) := union (replf x (fun x' => power (V x'))).
 
 Lemma V_morph : forall x x', x == x' -> V x == V x'.
 induction x; destruct x'; intros.
-simpl V; unfold replf; simpl sup.
+simpl V; unfold replf.
 apply union_morph.
 rewrite eq_set_def in H0; simpl in H0.
 destruct H0.

EnsEmUniv.v

@@ -322,6 +322,7 @@ refine (let (b,Hb) := S.intuit_repl_ax intuit
   apply U_intro.
 
   apply U_intro.
+  simpl in Hb.
 
  Texists (injU b).
   apply U_intro.
@@ -377,7 +378,7 @@ destruct S.collection_ax with a' (fun x y => R (injU x) (injU y)) as (B,HB).
  Tdestruct (H1 _ H2).
  apply down_in_ex with (1:=H0) in H2.
  Tdestruct H2.
- refine (let h := HB _ H5 _ in _).
+ simple refine (let h := HB _ H5 _ in _).
   apply U_elim in H3; Tdestruct H3.
   Texists x2.
   revert H4; apply H; apply B.eq_set_sym; trivial.

EnsLogic.v

@@ -469,8 +469,8 @@ destruct (choice_axiom {i:X|exists w, R i w} set (fun i y => R (proj1_sig i) y))
  exists {i:X|exists w, R i w}.
  exists f.
  intros.
- exists (existT _ i H).
- apply (Hf (existT _ i H)).
+ exists (exist _ i H).
+ apply (Hf (exist _ i H)).
 Qed.
 
 (* ttcoll rephrased on sets: *)
@@ -716,7 +716,7 @@ Fixpoint V (x:set) := union (replf x (fun x' => power (V x'))).
 
 Lemma V_morph : forall x x', x == x' -> V x == V x'.
 induction x; destruct x'; intros.
-simpl V; unfold replf; simpl sup.
+simpl V; unfold replf.
 apply union_morph.
 rewrite eq_set_def in H0; simpl in H0.
 destruct H0.

GenLemmas.v

@@ -205,7 +205,7 @@ assert (val_ok (A::e) (V.cons (int D i) i) (I.cons (tm D j) j)) by
   (apply vcons_add_var; trivial).
 apply red_typ with (1:=H) in HB; 
   [destruct HB as (HSB, HB)|destruct C; [discriminate|trivial]].
-apply in_int_intro; [destruct B; [discriminate|]| |]; trivial.
+apply SN.in_int_intro; [destruct B; [discriminate|]| |]; trivial.
 revert HB; apply real_morph.
  rewrite int_subst_eq; reflexivity.
 

GenRealSN.v

@@ -1146,7 +1146,7 @@ case_eq (nth_error e n); intros.
  apply typ_subsumption with (lift (S n) t); auto.
   apply typ_var; trivial.
 
-  destruct t as [(t,tm)|]; simpl; try discriminate.
+  destruct t as [(t,tm,?,?,?,?)|]; simpl; try discriminate.
   elim H; trivial.
 
   discriminate.

HFcoc.v

@@ -75,6 +75,7 @@ apply repl_ext; intros.
  rewrite H4 in H2.
  clear H4 x0.
  elim repl_elim with (1:=Pm'') (2 := H2); intros; clear H2.
+ cbv beta in H1.
  rewrite H5 in H1 |- *; rewrite snd_def; rewrite fst_def in H1.
  apply in_hf_reg_r with (F x1); auto.
 

InstInterp.v

@@ -10,23 +10,23 @@ Import SN_nat.
 
 Fixpoint intp_foterm t:=
   match t with
-  | Var i => Ref i
-  | Cst_0 => Zero
-  | Cst_1 => App Succ Zero
-  | Df_Add u v => App (App Add (intp_foterm u)) (intp_foterm v)
+  | Var' i => Ref i
+  | Cst_0' => Zero
+  | Cst_1' => App Succ Zero
+  | Df_Add' u v => App (App Add (intp_foterm u)) (intp_foterm v)
   end.
 
 Fixpoint intp_fofml f:=
   match f with
-  | eq_foterm x y => EQ_term (intp_foterm x) (intp_foterm y)
-  | TF => True_symb
-  | BF => False_symb
-  | neg f => Neg (intp_fofml f)
-  | conj f1 f2 => Conj (intp_fofml f1) (intp_fofml f2)
-  | disj f1 f2 => Disj (intp_fofml f1) (intp_fofml f2)
-  | implf f1 f2 => Impl (intp_fofml f1) (intp_fofml f2)
-  | fall f => Fall (intp_fofml f)
-  | exst f => Exst (intp_fofml f)
+  | eq_foterm' x y => EQ_term (intp_foterm x) (intp_foterm y)
+  | TF' => True_symb
+  | BF' => False_symb
+  | neg' f => Neg (intp_fofml f)
+  | conj' f1 f2 => Conj (intp_fofml f1) (intp_fofml f2)
+  | disj' f1 f2 => Disj (intp_fofml f1) (intp_fofml f2)
+  | implf' f1 f2 => Impl (intp_fofml f1) (intp_fofml f2)
+  | fall' f => Fall (intp_fofml f)
+  | exst' f => Exst (intp_fofml f)
   end.
 
 Lemma intp_eq_fml : forall x y, 

InstSem.v

@@ -1245,7 +1245,7 @@ assert (eq_term (lift_rec 1 0 Add) Add) as Hadd_lift.
       |unfold V.lams, V.shift; simpl; apply H].
      do 3 red; intros. apply app_ext; [apply app_ext; [reflexivity|]|]; trivial.
 
-    unfold I.lams, I.shift; simpl; do 2 rewrite H; trivial.
+    unfold I.lams, I.shift; simpl; rewrite H; trivial.
 
 rewrite Hadd_lift. do 2 (rewrite eq_term_lift_ref_fv; [simpl plus|omega]).
 setoid_replace (lift_rec 1 0 Succ) with Succ using relation eq_term by 

InstSyn.v

@@ -17,43 +17,43 @@ Definition Df_Add := Df_Add'.
 
 Fixpoint lift_term_rec t n k:=
   match t with
-    | Var i => 
+    | Var' i =>
       match le_gt_dec k i with
         | left _ => Var (i+n)
         | right _ => Var i
       end
-    | Cst_0 => Cst_0
-    | Cst_1 => Cst_1
-    | Df_Add u v => Df_Add (lift_term_rec u n k) (lift_term_rec v n k)
+    | Cst_0' => Cst_0
+    | Cst_1' => Cst_1
+    | Df_Add' u v => Df_Add (lift_term_rec u n k) (lift_term_rec v n k)
   end.
 
 Definition lift_term t n := lift_term_rec t n 0.
 
 Fixpoint subst_term_rec M N n:= 
   match M with
-    | Var i =>
+    | Var' i =>
       match lt_eq_lt_dec n i with
         | inleft (left _) => Var (pred i)
         | inleft (right _) => lift_term N n
         | inright _ => Var i
       end
-    | Cst_0 => Cst_0
-    | Cst_1 => Cst_1
-    | Df_Add M1 M2 => Df_Add (subst_term_rec M1 N n) (subst_term_rec M2 N n)
+    | Cst_0' => Cst_0
+    | Cst_1' => Cst_1
+    | Df_Add' M1 M2 => Df_Add (subst_term_rec M1 N n) (subst_term_rec M2 N n)
   end.
 
 Definition subst_term M N := subst_term_rec M N 0.
 
 Fixpoint fv_term_rec t k : list nat :=
   match t with
-    | Var n => 
+    | Var' n =>
       match le_gt_dec k n with
         | left _ => (n-k)::nil
         | right _ => nil
       end
-    | Cst_0 => nil
-    | Cst_1 => nil
-    | Df_Add M N => (fv_term_rec M k) ++ (fv_term_rec N k)
+    | Cst_0' => nil
+    | Cst_1' => nil
+    | Df_Add' M N => (fv_term_rec M k) ++ (fv_term_rec N k)
   end.
 
 Definition fv_term t := fv_term_rec t 0.
@@ -82,45 +82,45 @@ Definition exst := exst'.
 
 Fixpoint lift_fml_rec f n k:=
   match f with
-    | eq_foterm x y => eq_foterm (lift_term_rec x n k) (lift_term_rec y n k)
-    | TF => TF
-    | BF => BF
-    | neg f' => neg (lift_fml_rec f' n k)
-    | conj A B => conj (lift_fml_rec A n k) (lift_fml_rec B n k)
-    | disj A B => disj (lift_fml_rec A n k) (lift_fml_rec B n k)
-    | implf A B => implf (lift_fml_rec A n k) (lift_fml_rec B n k)
-    | fall A => fall (lift_fml_rec A n (S k))
-    | exst A => exst (lift_fml_rec A n (S k))
+    | eq_foterm' x y => eq_foterm (lift_term_rec x n k) (lift_term_rec y n k)
+    | TF' => TF
+    | BF' => BF
+    | neg' f' => neg (lift_fml_rec f' n k)
+    | conj' A B => conj (lift_fml_rec A n k) (lift_fml_rec B n k)
+    | disj' A B => disj (lift_fml_rec A n k) (lift_fml_rec B n k)
+    | implf' A B => implf (lift_fml_rec A n k) (lift_fml_rec B n k)
+    | fall' A => fall (lift_fml_rec A n (S k))
+    | exst' A => exst (lift_fml_rec A n (S k))
   end.
 
 Definition lift_fml t n := lift_fml_rec t n 0.
 
 Fixpoint subst_fml_rec f N n :=
   match f with
-    | eq_foterm x y => eq_foterm (subst_term_rec x N n) (subst_term_rec y N n)
-    | TF => TF
-    | BF => BF
-    | neg f => neg (subst_fml_rec f N n)
-    | conj f1 f2 => conj (subst_fml_rec f1 N n) (subst_fml_rec f2 N n)
-    | disj f1 f2 => disj (subst_fml_rec f1 N n) (subst_fml_rec f2 N n)
-    | implf f1 f2 => implf (subst_fml_rec f1 N n) (subst_fml_rec f2 N n)
-    | fall f => fall (subst_fml_rec f N (S n))
-    | exst f => exst (subst_fml_rec f N (S n))
+    | eq_foterm' x y => eq_foterm (subst_term_rec x N n) (subst_term_rec y N n)
+    | TF' => TF
+    | BF' => BF
+    | neg' f => neg (subst_fml_rec f N n)
+    | conj' f1 f2 => conj (subst_fml_rec f1 N n) (subst_fml_rec f2 N n)
+    | disj' f1 f2 => disj (subst_fml_rec f1 N n) (subst_fml_rec f2 N n)
+    | implf' f1 f2 => implf (subst_fml_rec f1 N n) (subst_fml_rec f2 N n)
+    | fall' f => fall (subst_fml_rec f N (S n))
+    | exst' f => exst (subst_fml_rec f N (S n))
   end.
 
 Definition subst_fml f N := subst_fml_rec f N 0.
 
 Fixpoint fv_fml_rec f k : list nat :=
   match f with
-    | eq_foterm t1 t2 => (fv_term_rec t1 k) ++ (fv_term_rec t2 k)
-    | TF => nil
-    | BF => nil
-    | neg f0 => fv_fml_rec f0 k
-    | conj f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k)
-    | disj f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k)
-    | implf f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k)
-    | fall f0 => (fv_fml_rec f0 (S k))
-    | exst f0 => (fv_fml_rec f0 (S k))
+    | eq_foterm' t1 t2 => (fv_term_rec t1 k) ++ (fv_term_rec t2 k)
+    | TF' => nil
+    | BF' => nil
+    | neg' f0 => fv_fml_rec f0 k
+    | conj' f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k)
+    | disj' f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k)
+    | implf' f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k)
+    | fall' f0 => (fv_fml_rec f0 (S k))
+    | exst' f0 => (fv_fml_rec f0 (S k))
   end.
 
 Definition fv_fml f := fv_fml_rec f 0.

Lambda.v

@@ -518,7 +518,7 @@ split; intros.
     destruct n; simpl; trivial.
     inversion l.
 
-    apply NPeano.Nat.lt_pred_le in g.
+    apply Nat.lt_pred_le in g.
     elim (Lt.lt_irrefl n).
     apply Lt.le_lt_trans with k; trivial.
 
@@ -1137,7 +1137,7 @@ induction M; simpl; intros.
  rewrite <- plus_n_Sm in H0.
  split; auto with arith.
  constructor.
- rewrite <- NPeano.Nat.sub_succ_l; trivial.
+ rewrite <- Nat.sub_succ_l; trivial.
  apply Le.le_trans with (m+k); auto with arith.
 
  inversion_clear H0.

ModelNat_ZFind.v

@@ -348,12 +348,3 @@ apply fa_morph; intros P.
 apply fa_morph; intros Pm.
 rewrite H1; rewrite H; reflexivity.
 Qed.
-
-red in H; specialize H with (1:=H0); simpl in H.
-rewrite cc_beta_eq; auto with *.
-rewrite NATREC_S; auto.
- reflexivity.
-
- do 2 red; intros; apply cc_app_morph; auto with *.
- apply cc_app_morph; auto with *.
-Qed.

Nest.v

@@ -1,4 +1,4 @@
-
+Require Export CoqCompat.
 (** Showing a nested inductive type operator is isomorphic to
     a W-type.
 *)

NonUniform.v

@@ -1,3 +1,4 @@
+Require Export CoqCompat.
 (** This file shows how big non-uniform parameters can be encoded
     as an index without changing the universe of the definition.
  *)