diff options
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 78ec8ff24..e9b90b52c 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -1308,11 +1308,11 @@ Qed. (**********************************************************************) (** * Compatibility notations *) Notation description_rel_choice_imp_funct_choice := - functional_rel_reification_and_rel_choice_imp_fun_choice (compat "8.6"). + functional_rel_reification_and_rel_choice_imp_fun_choice (only parsing). -Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (compat "8.6"). +Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (only parsing). Notation FunChoice_Equiv_RelChoice_and_ParamDefinDescr := - fun_choice_iff_rel_choice_and_functional_rel_reification (compat "8.6"). + fun_choice_iff_rel_choice_and_functional_rel_reification (only parsing). -Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (compat "8.6"). +Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (only parsing). |