messed up; fixed

Beluga-lang · Apr 26, 2024 · 5acfa9f · 5acfa9f
1 parent a171cc8
commit 5acfa9f
Showing 1 changed file with 0 additions and 10 deletions.
diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
@@ -58,13 +58,8 @@ Section Per_univ_elem_core_def.
   | per_univ_elem_core_nat : {{ DF ℕ ≈ ℕ ∈ per_univ_elem_core ↘ per_nat }}
   | per_univ_elem_core_pi :
     `{ forall (in_rel : relation domain)
-<<<<<<< HEAD
          (out_rel : forall {c c'}, {{ Dom c ≈ c' ∈ in_rel }} -> relation domain)
          (equiv_a_a' : {{ DF a ≈ a' ∈ per_univ_elem_core ↘ in_rel}}),
-=======
-          (out_rel : forall {c c'}, {{ Dom c ≈ c' ∈ in_rel }} -> relation domain)
-          (equiv_a_a' : {{ DF a ≈ a' ∈ per_univ_elem_core ↘ in_rel }}),
->>>>>>> 47fa52f5eb989104966e70555de900ab7ce0e164
           (forall {c c'} (equiv_c_c' : {{ Dom c ≈ c' ∈ in_rel }}),
               rel_mod_eval per_univ_elem_core B d{{{ p ↦ c }}} B' d{{{ p' ↦ c' }}} (out_rel equiv_c_c')) ->
           (forall f f', elem_rel f f' <-> forall {c c'} (equiv_c_c' : in_rel c c'),
@@ -118,7 +113,6 @@ Global Hint Constructors per_univ_elem_core : mcltt.
 
 Equations per_univ_elem (i : nat) : domain -> domain -> relation domain -> Prop by wf i :=
 | i => per_univ_elem_core i (fun j lt_j_i a a' => exists R', per_univ_elem j a a' R').
-<<<<<<< HEAD
 
 Definition per_univ (i : nat) : relation domain := fun a a' => exists R', per_univ_elem i a a' R'.
 
@@ -186,10 +180,6 @@ Definition per_univ_like (R : domain -> domain -> relation domain -> Prop) := fu
 #[global]
 Transparent per_univ_like.
 
-=======
-Definition per_univ (i : nat) : relation domain := fun a a' => exists R', per_univ_elem i a a' R'.
-
->>>>>>> 47fa52f5eb989104966e70555de900ab7ce0e164
 Definition rel_typ (i : nat) (A : typ) (p : env) (A' : typ) (p' : env) R' := rel_mod_eval (per_univ_elem i) A p A' p' R'.
 
 Inductive per_ctx_env : ctx -> ctx -> relation env -> Prop :=