diff options
| author | Guillaume Melquiond | 2015-07-26 07:44:45 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-07-26 07:44:45 +0200 |
| commit | beff9386b82c4aa6e066642d56a36c8034f54604 (patch) | |
| tree | e71dc5490327b5b3fdbc69167aecab4ddaee2b7b | |
| parent | 8a235780d9b3612e1c01323398da3e80cbbf8e9f (diff) | |
Remove obsolete question about eta-conversion.
| -rw-r--r-- | doc/faq/FAQ.tex | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 589933578a..d264ac62a5 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2579,12 +2579,6 @@ Qed. You can help {\Coq} using the {\pattern} tactic. -\Question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?} - - This is because \texttt{\{x:A|P x\}} is a notation for -\texttt{sig (fun x:A => P x)}. Since {\Coq} does not reason up to -$\eta$-conversion, this is different from \texttt{sig P}. - \Question{I copy-paste a term and {\Coq} says it is not convertible to the original term. Sometimes it even says the copied term is not |