diff options
| author | Maxime Dénès | 2017-08-29 14:45:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-29 14:45:47 +0200 |
| commit | 7caaf8d434499feb1c3b3c86ad1538905fc34d3f (patch) | |
| tree | b83067ea7085d119593fce282a7bf756de402825 /plugins/ltac/extratactics.ml4 | |
| parent | c3bc1fda9c5dd1805b23d04f2dee711aeec1f4a1 (diff) | |
| parent | 569a26809a3b5e72033aac29e9e2bc91f74f2092 (diff) | |
Merge PR #946: Functional pretyping interface
Diffstat (limited to 'plugins/ltac/extratactics.ml4')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index f3f2f27e9e..b847aadf21 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -40,7 +40,7 @@ let with_delayed_uconstr ist c tac = fail_evar = false; expand_evars = true } in - let c = Pretyping.type_uconstr ~flags ist c in + let c = Tacinterp.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac let replace_in_clause_maybe_by ist c1 c2 cl tac = @@ -359,7 +359,7 @@ let refine_tac ist simple with_classes c = let flags = { constr_flags () with Pretyping.use_typeclasses = with_classes } in let expected_type = Pretyping.OfType concl in - let c = Pretyping.type_uconstr ~flags ~expected_type ist c in + let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in let update = begin fun sigma -> c env sigma end in |