diff options
| author | Matthieu Sozeau | 2015-02-12 22:49:35 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-02-12 22:49:35 +0100 |
| commit | 8c5bfa0f00b80979473bba26c1b9a1410667e032 (patch) | |
| tree | 0857ce7a25ff85adcaa168a43edfed61a38470e0 | |
| parent | 5c603ebd99e4e8e7abb8b2036a6ffac5b19f66cf (diff) | |
Univs: fix bug #4031: wrong folding of sigma in change.
| -rw-r--r-- | tactics/tactics.ml | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4031.v | 14 |
2 files changed, 20 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a298bba978..04df3b8cda 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -569,8 +569,12 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env let sigma',ty' = redfun false env sigma ty in sigma', (id,None,ty') | Some b -> - let sigma',b' = if where != InHypTypeOnly then redfun true env sigma b else sigma, b in - let sigma',ty' = if where != InHypValueOnly then redfun false env sigma ty else sigma', ty in + let sigma',b' = + if where != InHypTypeOnly then redfun true env sigma b else sigma, b + in + let sigma',ty' = + if where != InHypValueOnly then redfun false env sigma' ty else sigma', ty + in sigma', (id,Some b',ty') let e_change_in_hyp redfun (id,where) = diff --git a/test-suite/bugs/closed/4031.v b/test-suite/bugs/closed/4031.v new file mode 100644 index 0000000000..2b8641ebb0 --- /dev/null +++ b/test-suite/bugs/closed/4031.v @@ -0,0 +1,14 @@ +Definition something (P:Type) (e:P) := e. + +Inductive myunit : Set := mytt. + (* Proof below works when definition is in Type, + however builtin types such as unit are in Set. *) + +Lemma demo_hide_generic : + let x := mytt in x = x. +Proof. + intros. + change mytt with (@something _ mytt) in x. + subst x. (* Proof works if this line is removed *) + reflexivity. +Qed.
\ No newline at end of file |