diff options
| author | letouzey | 2012-05-29 11:08:37 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:08:37 +0000 |
| commit | 5fa47f1258408541150e2e4c26d60ff694e7c1bc (patch) | |
| tree | 9e7aee1ea714cebdccc50dbd85735948d8baeaf0 /plugins/decl_mode/decl_proof_instr.ml | |
| parent | 45038a0bfd5621153ba0dd4b6e06755fd15da1e3 (diff) | |
locus.mli for occurrences+clauses, misctypes.mli for various little things
Corresponding operations in locusops.ml and miscops.ml
The type of occurrences is now a clear algebraic one instead of
a bool*list hard to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *) |