diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/rewrite.ml | 9 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 8 |
2 files changed, 9 insertions, 8 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 85c19fac40..3c6bd45637 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1526,7 +1526,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul | Success res -> let (_, cstrs) = res.rew_evars in let evars' = solve_constraints env res.rew_evars in - let newt = EConstr.of_constr (Evarutil.nf_evar evars' (EConstr.Unsafe.to_constr res.rew_to)) in + let newt = nf_evar evars' res.rew_to in let evars = (* Keep only original evars (potentially instantiated) and goal evars, the rest has been defined and substituted already. *) Evar.Set.fold @@ -2151,10 +2151,9 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite (** [setoid_]{reflexivity,symmetry,transitivity} tactics *) -let not_declared env ty rel = - let rel = EConstr.Unsafe.to_constr rel in +let not_declared env sigma ty rel = tclFAIL 0 - (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++ + (str" The relation " ++ Printer.pr_econstr_env env sigma rel ++ str" is not a declared " ++ str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library") let setoid_proof ty fn fallback = @@ -2181,7 +2180,7 @@ let setoid_proof ty fn fallback = begin match e with | (Not_found, _) -> let rel, _, _ = decompose_app_rel env sigma concl in - not_declared env ty rel + not_declared env sigma ty rel | (e, info) -> Proofview.tclZERO ~info e end | e' -> Proofview.tclZERO ~info e' diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 1fe6dbdd0b..d8df07733f 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -858,14 +858,16 @@ let rec message_of_value v = Ftactic.return (int (out_gen (topwit wit_int) v)) else if has_type v (topwit wit_intro_pattern) then let p = out_gen (topwit wit_intro_pattern) v in - let print env sigma c = pr_constr_env env sigma (EConstr.Unsafe.to_constr (fst (Tactics.run_delayed env Evd.empty c))) in + let print env sigma c = + let (c, sigma) = Tactics.run_delayed env sigma c in + pr_econstr_env env sigma c + in Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p) end } else if has_type v (topwit wit_constr_context) then let c = out_gen (topwit wit_constr_context) v in - let c = EConstr.Unsafe.to_constr c in - Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (project gl) c) end } + Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end } else if has_type v (topwit wit_uconstr) then let c = out_gen (topwit wit_uconstr) v in Ftactic.nf_enter { enter = begin fun gl -> |