diff options
| author | Pierre-Marie Pédrot | 2016-08-21 01:00:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-21 01:00:26 +0200 |
| commit | 6278ce16ab1b8b65c7d1770d265471f594c8e793 (patch) | |
| tree | 4e8eac6336e5a1848fdbb1103932c665cf334cca /tactics | |
| parent | 69a35378d37b8eb7e1019d24ab5e0fd27f25b6bc (diff) | |
| parent | 513e194656429b6a9142a3a34095cee2c6f8ee96 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 2c97cf4425..3e5b7b65ff 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -629,7 +629,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = in match evd with | None -> - tclFAIL 0 (str"Terms do not have convertible types.") + tclFAIL 0 (str"Terms do not have convertible types") | Some evd -> let e = build_coq_eq () in let sym = build_coq_eq_sym () in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9d08ada60a..acc0fa1ca7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1270,7 +1270,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) let naming = NamingMustBe (dloc,targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS clenv.evd) + (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) (if sidecond_first then Tacticals.New.tclTHENFIRST (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac |