diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/derive/derive.ml | 5 | ||||
-rw-r--r-- | plugins/firstorder/g_ground.ml4 | 6 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 13 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 6 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 28 | ||||
-rw-r--r-- | plugins/ltac/g_ltac.ml4 | 12 | ||||
-rw-r--r-- | plugins/ltac/pptactic.ml | 6 | ||||
-rw-r--r-- | plugins/ltac/profile_ltac.ml | 2 | ||||
-rw-r--r-- | plugins/ltac/profile_ltac_tactics.ml4 | 4 | ||||
-rw-r--r-- | plugins/ltac/rewrite.ml | 31 | ||||
-rw-r--r-- | plugins/ltac/tacexpr.mli | 2 | ||||
-rw-r--r-- | plugins/ltac/tacintern.ml | 4 | ||||
-rw-r--r-- | plugins/ltac/tacinterp.ml | 6 | ||||
-rw-r--r-- | plugins/ltac/tacsubst.ml | 2 | ||||
-rw-r--r-- | plugins/ltac/tactic_matching.ml | 4 | ||||
-rw-r--r-- | plugins/ssr/ssrcommon.ml | 1 | ||||
-rw-r--r-- | plugins/ssr/ssrequality.ml | 6 | ||||
-rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 6 | ||||
-rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 33 |
21 files changed, 94 insertions, 89 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index fb65a8639..c8c4c2dad 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -38,9 +38,8 @@ let start_deriving f suchthat lemma = let f_type = EConstr.Unsafe.to_constr f_type in let ef = EConstr.Unsafe.to_constr ef in let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in - let evdref = ref sigma in - let suchthat = Constrintern.interp_type_evars env' evdref suchthat in - TCons ( env' , !evdref , suchthat , (fun sigma _ -> + let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in + TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))))) in diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 938bec25b..b81010c7b 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -40,17 +40,17 @@ let _= in declare_int_option gdopt -let congruence_depth=ref 100 let _= + let congruence_depth=ref 100 in let gdopt= - { optdepr=false; + { optdepr=true; (* noop *) optname="Congruence Depth"; optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); optwrite= (function - None->congruence_depth:=0 + None->congruence_depth:=0 | Some i->congruence_depth:=(max i 0))} in declare_int_option gdopt diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index fa4353630..889c064b2 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1497,7 +1497,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) Decl_kinds.Finite with | UserError(s,msg) as e -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9e22ad306..071599d9c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -158,8 +158,8 @@ let build_newrecursive (fun (env,impls) (((_,recname),_),bl,arityc,_) -> let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in - let evdref = ref (Evd.from_env env0) in - let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in + let evd = Evd.from_env env0 in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in let open Context.Named.Declaration in (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) @@ -406,7 +406,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - Command.do_definition + ComDefinition.do_definition + ~program_mode:false fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); @@ -426,7 +427,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> @@ -616,8 +617,8 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in + let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in + let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8bf6e48fd..5a9248d47 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -183,7 +183,9 @@ let with_full_print f a = and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in let old_printuniverses = !Constrextern.print_universes in + let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in Constrextern.print_universes := true; + Detyping.print_allow_match_default_clause := false; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; @@ -197,6 +199,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); res with @@ -206,6 +209,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); raise reraise diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 9e2774ff3..9fcb35f89 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -889,11 +889,11 @@ let merge_inductive (ind1: inductive) (ind2: inductive) } in *) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) - let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,pl,impls = Command.interp_mutual_inductive indl [] + let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in + let mie,pl,impls = ComInductive.interp_mutual_inductive indl [] false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) + ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls) (* Find infos on identifier id. *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 766adfc63..363ad5dfc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1427,7 +1427,7 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let evmap, env = Pfedit.get_current_context () in + let evd, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; @@ -1479,13 +1479,13 @@ let (com_eqn : int -> Id.t -> | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let evmap, env = Pfedit.get_current_context () in - let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in + let evd, env = Pfedit.get_current_context () in + let evd = Evd.from_ctx (Evd.evar_universe_context evd) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) - evmap + evd (EConstr.of_constr equation_lemma_type) (Lemmas.mk_hook (fun _ _ -> ())); ignore (by @@ -1528,14 +1528,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let open Constr in let open CVars in let env = Global.env() in - let evd = ref (Evd.from_env env) in - let function_type = interp_type_evars env evd type_of_f in + let evd = Evd.from_env env in + let evd, function_type = interp_type_evars env evd type_of_f in let function_type = EConstr.Unsafe.to_constr function_type in let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let ty = interp_type_evars env evd ~impls:rec_impls eq in + let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in let ty = EConstr.Unsafe.to_constr ty in - let evm, nf = Evarutil.nf_evars_and_universes !evd in + let evd, nf = Evarutil.nf_evars_and_universes evd in let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in let function_type = nf function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in @@ -1560,16 +1560,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in + let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) - let evm = Evd.from_env (Global.env ()) in + let evd = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in let relation, evuctx = - interp_constr env_with_pre_rec_args evm r + interp_constr env_with_pre_rec_args evd r in - let evm = Evd.from_ctx evuctx in + let evd = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) @@ -1599,7 +1599,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num and functional_ref = destConst (constr_of_global functional_ref) and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr - functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation); + functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation); Flags.if_verbose msgnl (h 1 (Ppconstr.pr_id function_name ++ spc () ++ str"is defined" )++ fnl () ++ @@ -1618,5 +1618,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - evm (Lemmas.mk_hook hook)) + evd (Lemmas.mk_hook hook)) () diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 8b9eb3983..ebf6e450b 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 6aa2f6f89..e5ff47356 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/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 1f29f4860..5e3b7cf77 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -408,7 +408,7 @@ let print_results_filter ~cutoff ~filter = let results = SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in let results = merge_roots results Local.(CList.last !stack) in - Feedback.msg_notice (to_string ~cutoff ~filter results) + Feedback.msg_info (to_string ~cutoff ~filter results) ;; let print_results ~cutoff = diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 2b1106ee2..f09566063 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -13,7 +13,7 @@ open Profile_ltac open Stdarg -DECLARE PLUGIN "profile_ltac_plugin" +DECLARE PLUGIN "ltac_plugin" let tclSET_PROFILING b = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b)) @@ -22,7 +22,7 @@ TACTIC EXTEND start_ltac_profiling | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] END -TACTIC EXTEND stop_profiling +TACTIC EXTEND stop_ltac_profiling | [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] END diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c0060c5a7..a698b05dd 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 = @@ -1781,7 +1781,9 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = - new_instance (Flags.is_universe_polymorphism ()) + let program_mode = Flags.is_program_mode () in + let poly = Flags.is_universe_polymorphism () in + new_instance ~program_mode poly binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global ~generalize:false ~refine:false Hints.empty_hint_info @@ -2012,23 +2014,26 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~global:glob poly binders instance - (Some (true, CAst.make @@ CRecord [])) - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) + let program_mode = Flags.is_program_mode () in + ignore(new_instance ~program_mode ~global:glob poly binders instance + (Some (true, CAst.make @@ CRecord [])) + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) (** 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 +2068,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 +2089,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 9bd3efc6b..ccd555b61 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 b16b0a7ba..ebffde441 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 e25c99323..179952f28 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) @@ -890,7 +890,7 @@ let interp_intro_pattern_naming_option ist env sigma = function let interp_or_and_intro_pattern_option ist env sigma = function | None -> sigma, None | Some (ArgVar (loc,id)) -> - (match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with + (match interp_intro_pattern_var loc ist env sigma id with | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) | _ -> user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern.")) @@ -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 918d1faeb..79bf3685e 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 89b78e590..e87951dd7 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 diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 047ca509b..8493dbdbb 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1159,6 +1159,7 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) = let (c, ucst), cl = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1 with NoMatch -> redex_of_pattern env pat, (EConstr.Unsafe.to_constr cl) in + let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in let cl = EConstr.of_constr cl in let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index bd9633afb..6032ed2af 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -143,14 +143,14 @@ let newssrcongrtac arg ist gl = (** Coq rewrite compatibility flag *) -let ssr_strict_match = ref false let _ = - Goptions.declare_bool_option + let ssr_strict_match = ref false in + Goptions.declare_bool_option { Goptions.optname = "strict redex matching"; Goptions.optkey = ["Match"; "Strict"]; Goptions.optread = (fun () -> !ssr_strict_match); - Goptions.optdepr = false; + Goptions.optdepr = true; (* noop *) Goptions.optwrite = (fun b -> ssr_strict_match := b) } (** Rewrite rules *) diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 3efb7b914..4f530a0ae 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -74,7 +74,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; let no_ct = None, None and no_rt = None in let aliasvar = function - | [_, [{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) + | [[{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) | _ -> None in let mk_cnotype mp = aliasvar mp, None in let mk_ctype mp t = aliasvar mp, Some t in @@ -86,14 +86,14 @@ let mk_pat c (na, t) = (c, na, t) in GEXTEND Gram GLOBAL: binder_constr; ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]]; - ssr_mpat: [[ p = pattern -> [Loc.tag ~loc:!@loc [p]] ]]; + ssr_mpat: [[ p = pattern -> [[p]] ]]; ssr_dpat: [ [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> mp, mk_ctype mp t, rt | mp = ssr_mpat; rt = ssr_rtype -> mp, mk_cnotype mp, rt | mp = ssr_mpat -> mp, no_ct, no_rt ] ]; ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]]; - ssr_elsepat: [[ "else" -> [Loc.tag ~loc:!@loc [CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; + ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]]; binder_constr: [ [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index e63a05b78..d6dbad7a9 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1228,7 +1228,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in match pattern with - | None -> do_subst env0 concl0 concl0 1 + | None -> do_subst env0 concl0 concl0 1, Evd.empty_evar_universe_context | Some (sigma, (T rp | In_T rp)) -> let rp = fs sigma rp in let ise = create_evar_defs sigma in @@ -1236,8 +1236,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in let concl = find_T env0 concl0 1 ~k:do_subst in - let _ = end_T () in - concl + let _, _, (_, us, _) = end_T () in + concl, us | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) -> let p = fs sigma p in let occ = match pattern with Some (_, X_In_T _) -> occ | _ -> noindex in @@ -1252,8 +1252,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h ~k:(fun env _ -> do_subst env e_body))) in - let _ = end_X () in let _ = end_T () in - concl + let _ = end_X () in let _, _, (_, us, _) = end_T () in + concl, us | Some (sigma, E_In_X_In_T (e, hole, p)) -> let p, e = fs sigma p, fs sigma e in let ex = ex_value hole in @@ -1268,8 +1268,9 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h -> find_E env e_body h ~k:do_subst))) in - let _ = end_E () in let _ = end_X () in let _ = end_T () in - concl + let _,_,(_,us,_) = end_E () in + let _ = end_X () in let _ = end_T () in + concl, us | Some (sigma, E_As_X_In_T (e, hole, p)) -> let p, e = fs sigma p, fs sigma e in let ex = ex_value hole in @@ -1287,8 +1288,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let e_sigma = unify_HO env sigma (EConstr.of_constr e_body) (EConstr.of_constr e) in let e_body = fs e_sigma e in do_subst env e_body e_body h))) in - let _ = end_X () in let _ = end_TE () in - concl + let _ = end_X () in let _,_,(_,us,_) = end_TE () in + concl, us ;; let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = @@ -1306,12 +1307,14 @@ let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = let find_R, conclude = let r = ref None in (fun env c _ h' -> - do_once r (fun () -> c, Evd.empty_evar_universe_context); + do_once r (fun () -> c); if do_make_rel then mkRel (h'+h-1) else c), - (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in - let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in + (fun _ -> if !r = None then fst(redex_of_pattern env pat) + else assert_done r) in + let cl, us = + eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in let e = conclude cl in - e, cl + (e, us), cl ;; (* clenup interface for external use *) @@ -1319,6 +1322,10 @@ let mk_tpattern ?p_origin env sigma0 sigma_t f dir c = mk_tpattern ?p_origin env sigma0 sigma_t f dir c ;; +let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = + fst (eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst) +;; + let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let p = EConstr.Unsafe.to_constr p in let concl = EConstr.Unsafe.to_constr concl in |