diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-09 18:43:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-10 11:16:35 +0100 |
| commit | 08fa634493b8635a77174bbdcd0e1529e3c40279 (patch) | |
| tree | 22605ad884683c0da4d0b2f41de8339bb7f3d2e1 | |
| parent | b3aba0467a99ce8038816b845cf883be3521fce8 (diff) | |
Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly.
| -rw-r--r-- | tactics/tactics.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 37b715ebe..0a013e95f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2345,7 +2345,12 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let t = match ty with Some t -> t | _ -> typ_of env sigma c in + let (sigma, t) = match ty with + | Some t -> (sigma, t) + | None -> + let t = typ_of env sigma c in + Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t + in let eq_tac gl = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with |