diff options
Diffstat (limited to 'plugins/decl_mode/decl_proof_instr.ml')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 2870e8f7e1..956a561aa6 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -29,7 +29,7 @@ open Termops open Namegen open Reductionops open Goptions - +open Misctypes (* Strictness option *) @@ -237,7 +237,7 @@ let add_justification_hyps keep items gls = | _ -> let id=pf_get_new_id local_hyp_prefix gls in keep:=Idset.add id !keep; - tclTHEN (letin_tac None (Names.Name id) c None Tacexpr.nowhere) + tclTHEN (letin_tac None (Names.Name id) c None Locusops.nowhere) (thin_body [id]) gls in tclMAP add_aux items gls @@ -750,7 +750,7 @@ let consider_tac c hyps gls = | _ -> let id = pf_get_new_id (id_of_string "_tmp") gls in tclTHEN - (forward None (Some (dummy_loc, Genarg.IntroIdentifier id)) c) + (forward None (Some (dummy_loc, IntroIdentifier id)) c) (consider_match false [] [id] hyps) gls @@ -781,7 +781,7 @@ let rec build_function args body = let define_tac id args body gls = let t = build_function args body in - letin_tac None (Name id) t None Tacexpr.nowhere gls + letin_tac None (Name id) t None Locusops.nowhere gls (* tactics for reconsider *) |