diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-29 08:27:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-29 08:27:03 +0000 |
| commit | 7e2f953c3c19904616c43990fada92e762aadec9 (patch) | |
| tree | 8268d6e2b66ccdcce69df129ed98703e87f141b0 /test-suite/success/replace.v | |
| parent | ee711f8994d5e2e94cc61292ac6aab125c23df1c (diff) | |
Made tclABSTRACT normalize evars before saying it does not support
them. This was the cause of the failure of compilation of
CyclicAxioms after "replace" starting supporting open constrs (r13206).
Seized the opportunity to clean a little bit things around nf_evar,
whd_evar, check_evars, etc.
Removed obsolete printer mod_self_id from dev/db.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/replace.v')
| -rw-r--r-- | test-suite/success/replace.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/replace.v b/test-suite/success/replace.v index 6acdd5161..0b112937e 100644 --- a/test-suite/success/replace.v +++ b/test-suite/success/replace.v @@ -22,3 +22,11 @@ replace x with 0 in H,H0 |- * . Undo. Admitted. +(* This failed at some point when "replace" started to support arguments + with evars but "abstract" did not supported any evars even defined ones *) + +Class U. +Lemma l (u : U) (f : U -> nat) (H : 0 = f u) : f u = 0. +replace (f _) with 0 by abstract apply H. +reflexivity. +Qed. |