diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/contradiction.ml | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 1 |
3 files changed, 2 insertions, 3 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index f8cca076f8..c4cf7b62f4 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -22,7 +22,7 @@ open Glob_term let absurd c gls = let env = pf_env gls and sigma = project gls in - let _,j = Coercion.Default.inh_coerce_to_sort dummy_loc env + let _,j = Coercion.inh_coerce_to_sort dummy_loc env (Evd.create_goal_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in let c = j.Environ.utj_val in (tclTHENS diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 9c0d5db2c6..66c59ec362 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -588,7 +588,7 @@ let hResolve id c occ t gl = let t_raw = Detyping.detype true env_ids env_names t in let rec resolve_hole t_hole = try - Pretyping.Default.understand sigma env t_hole + Pretyping.understand sigma env t_hole with | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) -> resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d4a7be4ecb..cf93a66cfb 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -44,7 +44,6 @@ open Printer open Inductiveops open Syntax_def open Pretyping -open Pretyping.Default open Extrawit open Pcoq open Compat |