diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 12 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 20 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tactic_matching.ml | 4 |
8 files changed, 22 insertions, 32 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 8b9eb39837..ebf6e450b1 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -78,11 +78,6 @@ let test_bracket_ident = let hint = G_proofs.hint -let warn_deprecated_appcontext = - CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated" - (fun () -> strbrk "appcontext is deprecated and will be removed " ++ - strbrk "in a future version") - GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint tactic_mode constr_may_eval constr_eval toplevel_selector @@ -242,12 +237,7 @@ GEXTEND Gram match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - let mode = not (!Flags.tactic_context_compat) in - Subterm (mode, oid, pc) - | IDENT "appcontext"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> - warn_deprecated_appcontext ~loc:!@loc (); - Subterm (true,oid, pc) + Subterm (oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6aa2f6f898..e5ff473568 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -526,11 +526,9 @@ let pr_goal_selector ~toplevel s = let pr_match_pattern pr_pat = function | Term a -> pr_pat a - | Subterm (b,None,a) -> - (** ppedrot: we don't make difference between [appcontext] and [context] - anymore, and the interpretation is governed by a flag instead. *) + | Subterm (None,a) -> keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]" - | Subterm (b,Some id,a) -> + | Subterm (Some id,a) -> keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]" let pr_match_hyps pr_pat = function diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c0060c5a7c..2e14243d8a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -361,8 +361,8 @@ end) = struct end (* let my_type_of env evars c = Typing.e_type_of env evars c *) -(* let mytypeofkey = Profile.declare_profile "my_type_of";; *) -(* let my_type_of = Profile.profile3 mytypeofkey my_type_of *) +(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *) +(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *) let type_app_poly env env evd f args = @@ -2021,14 +2021,16 @@ let add_morphism glob binders m s n = (** Taken from original setoid_replace, to emulate the old rewrite semantics where lemmas are first instantiated and then rewrite proceeds. *) -let check_evar_map_of_evars_defs evd = +let check_evar_map_of_evars_defs env evd = let metas = Evd.meta_list evd in let check_freemetas_is_empty rebus = Evd.Metaset.iter (fun m -> - if Evd.meta_defined evd m then () else - raise - (Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m]))) + if Evd.meta_defined evd m then () + else begin + raise + (Logic.RefinerError (env, evd, Logic.UnresolvedBindings [Evd.meta_name evd m])) + end) in List.iter (fun (_,binding) -> @@ -2063,7 +2065,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = let c1 = if l2r then nf c' else nf c1 and c2 = if l2r then nf c2 else nf c' and car = nf car and rel = nf rel in - check_evar_map_of_evars_defs sigma; + check_evar_map_of_evars_defs env sigma; let prf = nf prf in let prfty = nf (Retyping.get_type_of env sigma prf) in let sort = sort_of_rel env sigma but in @@ -2084,8 +2086,8 @@ let get_hyp gl (c,l) clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -(* let rewriteclaustac_key = Profile.declare_profile "cl_rewrite_clause_tac";; *) -(* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) +(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *) +(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 9bd3efc6b7..ccd555b615 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -81,7 +81,7 @@ type 'a with_bindings_arg = clear_flag * 'a with_bindings (* Type of patterns *) type 'a match_pattern = | Term of 'a - | Subterm of bool * Id.t option * 'a + | Subterm of Id.t option * 'a (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index b16b0a7bae..ebffde441d 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -428,9 +428,9 @@ let intern_hyp_location ist ((occs,id),hl) = (* Reads a pattern *) let intern_pattern ist ?(as_type=false) ltacvars = function - | Subterm (b,ido,pc) -> + | Subterm (ido,pc) -> let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in - ido, metas, Subterm (b,ido,pc) + ido, metas, Subterm (ido,pc) | Term pc -> let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in None, metas, Term pc diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index e0d7eca5f8..32a3b53fd8 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -420,7 +420,7 @@ let interp_hyp ist env sigma (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id)) + else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env sigma (loc,id as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) @@ -1040,7 +1040,7 @@ let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) = (bvars,instantiate_pattern env sigma lfun pat) let read_pattern lfun ist env sigma = function - | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) + | Subterm (ido,c) -> Subterm (ido,eval_pattern lfun ist env sigma c) | Term c -> Term (eval_pattern lfun ist env sigma c) (* Reads the hypotheses of a Match Context rule *) diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 918d1faebe..79bf3685e2 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -121,7 +121,7 @@ let subst_raw_may_eval subst = function | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c) let subst_match_pattern subst = function - | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc)) + | Subterm (ido,pc) -> Subterm (ido,(subst_glob_constr_or_pattern subst pc)) | Term pc -> Term (subst_glob_constr_or_pattern subst pc) let rec subst_match_goal_hyps subst = function diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 89b78e5907..e87951dd7f 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -237,7 +237,7 @@ module PatternMatching (E:StaticEnvironment) = struct return lhs with Constr_matching.PatternMatchingFailure -> fail end - | Subterm (with_app_context,id_ctxt,p) -> + | Subterm (id_ctxt,p) -> let rec map s (e, info) = { stream = fun k ctx -> match IStream.peek s with @@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx) } in - map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error + map (Constr_matching.match_subterm E.env E.sigma p term) imatching_error (** [rule_match_term term rule] matches the term [term] with the |