m

compiler/src/compiler/CustomFix.v

@@ -2,7 +2,7 @@
    Most of the file is nearly-verbatim copied from the stdlib file where Fix_eq is proven.
    The main goal is to get general recursion even when some arguments to the recursive function is a function (without using funext). *)
 
-(*Here we have, supposedly, maximum generality: dependent types and arbitrary equivalence relations*)
+(*Here we have, supposedly, maximum generality: dependent types and arbitrary relations*)
 Section GeneralFixPoint.
   Variable A : Type.
   Variable R : A -> A -> Prop.
@@ -48,7 +48,7 @@ Section GeneralFixPoint.
   Qed.
 End GeneralFixPoint.
 
-(*Here we have equivalence relations but no dependent types.*)
+(*Here we have arbitrary relations but no dependent types.*)
 Section NonDepFixPoint.
   Variable A : Type.
   Variable R : A -> A -> Prop.
@@ -68,7 +68,7 @@ Section NonDepFixPoint.
   Definition Fix_eq'_nondep := Fix_eq' A R Rwf (fun _ => P) F E1 (fun _ _ => E2) F_ext.
 End NonDepFixPoint.
 
-(*Here we have dependent types but equivalence relations are eq.
+(*Here we have dependent types but the relations are eq.
   Sadly we can't simply deduce these lemmas from the supposedly-general case,
   since there's no good way of instantiating E2 to get eq.*)
 Section EqualityFixPoint.