diff options
Diffstat (limited to 'plugins')
30 files changed, 212 insertions, 233 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 23f8fe04a3..ac2058ba1b 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -115,7 +115,7 @@ module Bool = struct | Case (info, r, _iv, arg, pats) -> let is_bool = let i = info.ci_ind in - Names.eq_ind i (Lazy.force ind) + Names.Ind.CanOrd.equal i (Lazy.force ind) in if is_bool then Ifb ((aux arg), (aux pats.(0)), (aux pats.(1))) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 6f5c910297..129b220680 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -145,7 +145,7 @@ let rec term_equal t1 t2 = | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2 | Constructor {ci_constr=(c1,u1); ci_arity=i1; ci_nhyps=j1}, Constructor {ci_constr=(c2,u2); ci_arity=i2; ci_nhyps=j2} -> - Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 (* FIXME check eq? *) + Int.equal i1 i2 && Int.equal j1 j2 && Construct.CanOrd.equal c1 c2 (* FIXME check eq? *) | _ -> false open Hashset.Combine @@ -155,7 +155,7 @@ let rec hash_term = function | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2) | Eps i -> combine 3 (Id.hash i) | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2) - | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j + | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (Construct.CanOrd.hash c) i j type ccpattern = PApp of term * ccpattern list (* arguments are reversed *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 2dca1d5e49..6869f9c47e 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -741,7 +741,7 @@ and extract_cst_app env sg mle mlt kn args = (* Can we instantiate types variables for this constant ? *) (* In Ocaml, inside the definition of this constant, the answer is no. *) let instantiated = - if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints + if lang () == Ocaml && List.mem_f Constant.CanOrd.equal kn !current_fixpoints then var2var' (snd schema) else instantiation schema in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index b1ce10985a..21ec80abbc 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -685,7 +685,7 @@ let is_regular_match br = | _ -> raise Impossible in let is_ref i tr = match get_r tr with - | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) + | GlobRef.ConstructRef (ind', j) -> Ind.CanOrd.equal ind ind' && Int.equal j (i + 1) | _ -> false in Array.for_all_i is_ref 0 br diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f8449bcda1..e56d66ca2d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -32,7 +32,7 @@ module Refset' = GlobRef.Set_env let occur_kn_in_ref kn = let open GlobRef in function | IndRef (kn',_) - | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' + | ConstructRef ((kn',_),_) -> MutInd.CanOrd.equal kn kn' | ConstRef _ | VarRef _ -> false let repr_of_r = let open GlobRef in function diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index f13901c36d..4adad53899 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -38,7 +38,7 @@ let compare_gr id1 id2 = if id1==id2 then 0 else if id1==dummy_id then 1 else if id2==dummy_id then -1 - else GlobRef.Ordered.compare id1 id2 + else GlobRef.CanOrd.compare id1 id2 module OrderedInstance= struct diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index db3631daa4..99c5f85125 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -62,7 +62,7 @@ module Hitem= struct type t = h_item let compare (id1,co1) (id2,co2)= - let c = GlobRef.Ordered.compare id1 id2 in + let c = GlobRef.CanOrd.compare id1 id2 in if c = 0 then let cmp (i1, c1) (i2, c2) = let c = Int.compare i1 i2 in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index e50c6087bb..73eb943418 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -674,7 +674,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos |Prod _ -> let new_infos = {dyn_infos with info = (f, args)} in build_proof_args env sigma do_finalize new_infos - | Const (c, _) when not (List.mem_f Constant.equal c fnames) -> + | Const (c, _) when not (List.mem_f Constant.CanOrd.equal c fnames) -> let new_infos = {dyn_infos with info = (f, args)} in (* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) build_proof_args env sigma do_finalize new_infos diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1ab747ca09..0ab9ac65d7 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -100,8 +100,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in let is_dom c = match Constr.kind c with - | Ind ((u, _), _) -> MutInd.equal u rel_as_kn - | Construct (((u, _), _), _) -> MutInd.equal u rel_as_kn + | Ind ((u, _), _) -> Environ.QMutInd.equal env u rel_as_kn + | Construct (((u, _), _), _) -> Environ.QMutInd.equal env u rel_as_kn | _ -> false in let get_fun_num c = diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index bbc4df7dde..ca6ae150a7 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -147,19 +147,19 @@ END module Vernac = Pvernac.Vernac_ module Tactic = Pltac -let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) = - Genarg.create_arg "function_rec_definition_loc" +let (wit_function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) = + Genarg.create_arg "function_fix_definition" -let function_rec_definition_loc = - Pcoq.create_generic_entry2 "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) +let function_fix_definition = + Pcoq.create_generic_entry2 "function_fix_definition" (Genarg.rawwit wit_function_fix_definition) } GRAMMAR EXTEND Gram - GLOBAL: function_rec_definition_loc ; + GLOBAL: function_fix_definition ; - function_rec_definition_loc: - [ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]] + function_fix_definition: + [ [ g = Vernac.fix_definition -> { Loc.tag ~loc g } ]] ; END @@ -168,7 +168,7 @@ END let () = let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in - Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer + Pptactic.declare_extra_vernac_genarg_pprule wit_function_fix_definition raw_printer let is_proof_termination_interactively_checked recsl = List.exists (function @@ -196,7 +196,7 @@ let is_interactive recsl = } VERNAC COMMAND EXTEND Function STATE CUSTOM -| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] +| ["Function" ne_function_fix_definition_list_sep(recsl,"with")] => { classify_funind recsl } -> { if is_interactive recsl then diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 012fcee486..314c8abcaf 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1316,9 +1316,9 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list = let prop_sort = Sorts.InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in + let eq c1 c2 = Environ.QConstant.equal env c1 c2 in List.map - (function - | cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes) + (function cst -> List.assoc_f eq (fst cst) this_block_funs_indexes) funs in let ind_list = @@ -2228,7 +2228,8 @@ let build_case_scheme fa = let prop_sort = Sorts.InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc_f Constant.equal funs this_block_funs_indexes + let eq c1 c2 = Environ.QConstant.equal env c1 c2 in + List.assoc_f eq funs this_block_funs_indexes in let ind, sf = let ind = (first_fun_kn, funs_indexes) in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6ed61043f9..767a9ec39b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -332,7 +332,7 @@ let add_pat_variables sigma pat typ env : Environ.env = let constructors = Inductiveops.get_constructors env indf in let constructor : Inductiveops.constructor_summary = List.find - (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) + (fun cs -> Construct.CanOrd.equal c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in let cs_args_types : types list = @@ -402,7 +402,8 @@ let rec pattern_to_term_and_type env typ = let constructors = Inductiveops.get_constructors env indf in let constructor = List.find - (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) + (fun cs -> + Construct.CanOrd.equal (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in let cs_args_types : types list = diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 8e1331ace9..164a446fe3 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -444,7 +444,8 @@ let rec are_unifiable_aux = function match (DAst.get l, DAst.get r) with | PatVar _, _ | _, PatVar _ -> are_unifiable_aux eqs | PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) -> - if not (eq_constructor constructor2 constructor1) then raise NotUnifiable + if not (Construct.CanOrd.equal constructor2 constructor1) then + raise NotUnifiable else let eqs' = try List.combine cpl1 cpl2 @ eqs @@ -464,7 +465,8 @@ let rec eq_cases_pattern_aux = function match (DAst.get l, DAst.get r) with | PatVar _, PatVar _ -> eq_cases_pattern_aux eqs | PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) -> - if not (eq_constructor constructor2 constructor1) then raise NotUnifiable + if not (Construct.CanOrd.equal constructor2 constructor1) then + raise NotUnifiable else let eqs' = try List.combine cpl1 cpl2 @ eqs diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 5d631aac84..118a917381 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -27,12 +27,13 @@ open Indfun_common *) let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl -> + let env = Proofview.Goal.env gl in let sigma = project gl in let typ = pf_get_hyp_typ hid gl in match EConstr.kind sigma typ with | App (i, args) when isInd sigma i -> let ((kn', num) as ind'), u = destInd sigma i in - if MutInd.equal kn kn' then + if Environ.QMutInd.equal env kn kn' then (* We have generated a graph hypothesis so that we must change it if we can *) let info = match find_Function_of_graph ind' with diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index ad4374dba3..ff4a82f864 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -41,7 +41,7 @@ let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simpl let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in - Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5) + Tacentries.create_ltac_quotation "ltac" inject (Pltac.ltac_expr, Some 5) (** Backward-compatible tactic notation entry names *) diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 6cf5d30a95..c38a4dcd90 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -74,22 +74,22 @@ let hint = G_proofs.hint } GRAMMAR EXTEND Gram - GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint + GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_value command hint tactic_mode constr_may_eval constr_eval toplevel_selector - operconstr; + term; tactic_then_last: - [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" -> + [ [ "|"; lta = LIST0 (OPT ltac_expr) SEP "|" -> { Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) } | -> { [||] } ] ] ; - tactic_then_gen: - [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) } - | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) } + for_each_goal: + [ [ ta = ltac_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (ta::first, last) } + | ta = ltac_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) } | ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) } - | ta = tactic_expr -> { ([ta], None) } - | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) } + | ta = ltac_expr -> { ([ta], None) } + | "|"; tg = for_each_goal -> { let (first,last) = tg in (TacId [] :: first, last) } | -> { ([TacId []], None) } ] ] ; @@ -97,13 +97,13 @@ GRAMMAR EXTEND Gram for [TacExtend] *) [ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ] ; - tactic_expr: + ltac_expr: [ "5" RIGHTA [ te = binder_tactic -> { te } ] | "4" LEFTA - [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) } - | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) } - | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> { + [ ta0 = ltac_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) } + | ta0 = ltac_expr; ";"; ta1 = ltac_expr -> { TacThen (ta0,ta1) } + | ta0 = ltac_expr; ";"; l = tactic_then_locality; tg = for_each_goal; "]" -> { let (first,tail) = tg in match l , tail with | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) @@ -111,51 +111,51 @@ GRAMMAR EXTEND Gram | false , None -> TacThen (ta0,TacDispatch first) | true , None -> TacThens (ta0,first) } ] | "3" RIGHTA - [ IDENT "try"; ta = tactic_expr -> { TacTry ta } - | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) } - | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) } - | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) } - | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta } - | IDENT "progress"; ta = tactic_expr -> { TacProgress ta } - | IDENT "once"; ta = tactic_expr -> { TacOnce ta } - | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta } - | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta } + [ IDENT "try"; ta = ltac_expr -> { TacTry ta } + | IDENT "do"; n = int_or_var; ta = ltac_expr -> { TacDo (n,ta) } + | IDENT "timeout"; n = int_or_var; ta = ltac_expr -> { TacTimeout (n,ta) } + | IDENT "time"; s = OPT string; ta = ltac_expr -> { TacTime (s,ta) } + | IDENT "repeat"; ta = ltac_expr -> { TacRepeat ta } + | IDENT "progress"; ta = ltac_expr -> { TacProgress ta } + | IDENT "once"; ta = ltac_expr -> { TacOnce ta } + | IDENT "exactly_once"; ta = ltac_expr -> { TacExactlyOnce ta } + | IDENT "infoH"; ta = ltac_expr -> { TacShowHyps ta } (*To do: put Abstract in Refiner*) | IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) } | IDENT "abstract"; tc = NEXT; "using"; s = ident -> { TacAbstract (tc,Some s) } - | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ] + | IDENT "only"; sel = selector; ":"; ta = ltac_expr -> { TacSelect (sel, ta) } ] (*End of To do*) | "2" RIGHTA - [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) } - | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) } - | IDENT "tryif" ; ta = tactic_expr ; - "then" ; tat = tactic_expr ; - "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) } - | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) } - | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ] + [ ta0 = ltac_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) } + | ta0 = ltac_expr; "+"; ta1 = ltac_expr -> { TacOr (ta0,ta1) } + | IDENT "tryif" ; ta = ltac_expr ; + "then" ; tat = ltac_expr ; + "else" ; tae = ltac_expr -> { TacIfThenCatch(ta,tat,tae) } + | ta0 = ltac_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) } + | ta0 = ltac_expr; "||"; ta1 = ltac_expr -> { TacOrelse (ta0,ta1) } ] | "1" RIGHTA [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> { TacMatchGoal (b,false,mrl) } | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; mrl = match_context_list; "end" -> { TacMatchGoal (b,true,mrl) } - | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> + | b = match_key; c = ltac_expr; "with"; mrl = match_list; "end" -> { TacMatch (b,c,mrl) } - | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + | IDENT "first" ; "["; l = LIST0 ltac_expr SEP "|"; "]" -> { TacFirst l } - | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + | IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" -> { TacSolve l } | IDENT "idtac"; l = LIST0 message_token -> { TacId l } | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ]; l = LIST0 message_token -> { TacFail (g,n,l) } | st = simple_tactic -> { st } - | a = tactic_arg -> { TacArg(CAst.make ~loc a) } - | r = reference; la = LIST0 tactic_arg_compat -> + | a = tactic_value -> { TacArg(CAst.make ~loc a) } + | r = reference; la = LIST0 tactic_arg -> { TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ] | "0" - [ "("; a = tactic_expr; ")" -> { a } - | "["; ">"; tg = tactic_then_gen; "]" -> { + [ "("; a = ltac_expr; ")" -> { a } + | "["; ">"; tg = for_each_goal; "]" -> { let (tf,tail) = tg in begin match tail with | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) @@ -166,24 +166,24 @@ GRAMMAR EXTEND Gram failkw: [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ] ; - (* binder_tactic: level 5 of tactic_expr *) + (* binder_tactic: level 5 of ltac_expr *) binder_tactic: [ RIGHTA - [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> + [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac_expr LEVEL "5" -> { TacFun (it,body) } | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ]; llc = LIST1 let_clause SEP "with"; "in"; - body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ] + body = ltac_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ] ; (* Tactic arguments to the right of an application *) - tactic_arg_compat: - [ [ a = tactic_arg -> { a } + tactic_arg: + [ [ a = tactic_value -> { a } | c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) } (* Unambiguous entries: tolerated w/o "ltac:" modifier *) | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ] ; (* Can be used as argument and at toplevel in tactic expressions. *) - tactic_arg: + tactic_value: [ [ c = constr_eval -> { ConstrMayEval c } | IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l } | IDENT "type_term"; c=uconstr -> { TacPretype c } @@ -223,20 +223,20 @@ GRAMMAR EXTEND Gram | l = ident -> { Name.Name l } ] ] ; let_clause: - [ [ idr = identref; ":="; te = tactic_expr -> + [ [ idr = identref; ":="; te = ltac_expr -> { (CAst.map (fun id -> Name id) idr, arg_of_expr te) } - | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr -> + | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = ltac_expr -> { (na, arg_of_expr te) } - | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + | idr = identref; args = LIST1 input_fun; ":="; te = ltac_expr -> { (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ] ; match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> + "["; pc = Constr.cpattern; "]" -> { Subterm (oid, pc) } - | pc = Constr.lconstr_pattern -> { Term pc } ] ] + | pc = Constr.cpattern -> { Term pc } ] ] ; - match_hyps: + match_hyp: [ [ na = name; ":"; mp = match_pattern -> { Hyp (na, mp) } | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) } | na = name; ":="; mpv = match_pattern -> @@ -250,19 +250,19 @@ GRAMMAR EXTEND Gram ] ] ; match_context_rule: - [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "=>"; te = tactic_expr -> { Pat (largs, mp, te) } - | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) } - | "_"; "=>"; te = tactic_expr -> { All te } ] ] + [ [ largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern; + "=>"; te = ltac_expr -> { Pat (largs, mp, te) } + | "["; largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern; + "]"; "=>"; te = ltac_expr -> { Pat (largs, mp, te) } + | "_"; "=>"; te = ltac_expr -> { All te } ] ] ; match_context_list: [ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl } | "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ] ; match_rule: - [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) } - | "_"; "=>"; te = tactic_expr -> { All te } ] ] + [ [ mp = match_pattern; "=>"; te = ltac_expr -> { Pat ([],mp,te) } + | "_"; "=>"; te = ltac_expr -> { All te } ] ] ; match_list: [ [ mrl = LIST1 match_rule SEP "|" -> { mrl } @@ -282,13 +282,13 @@ GRAMMAR EXTEND Gram (* Definitions for tactics *) tacdef_body: [ [ name = Constr.global; it=LIST1 input_fun; - redef = ltac_def_kind; body = tactic_expr -> + redef = ltac_def_kind; body = ltac_expr -> { if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in Tacexpr.TacticDefinition (id, TacFun (it, body)) } | name = Constr.global; redef = ltac_def_kind; - body = tactic_expr -> + body = ltac_expr -> { if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in @@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram ] ] ; tactic: - [ [ tac = tactic_expr -> { tac } ] ] + [ [ tac = ltac_expr -> { tac } ] ] ; range_selector: @@ -314,15 +314,12 @@ GRAMMAR EXTEND Gram { let open Goal_select in Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ] ; - selector_body: + selector: [ [ l = range_selector_or_nth -> { l } | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ] ; - selector: - [ [ IDENT "only"; sel = selector_body; ":" -> { sel } ] ] - ; toplevel_selector: - [ [ sel = selector_body; ":" -> { sel } + [ [ sel = selector; ":" -> { sel } | "!"; ":" -> { Goal_select.SelectAlreadyFocused } | IDENT "all"; ":" -> { Goal_select.SelectAll } ] ] ; @@ -343,8 +340,8 @@ GRAMMAR EXTEND Gram tac = Pltac.tactic -> { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ] ; - operconstr: LEVEL "0" - [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> + term: LEVEL "0" + [ [ IDENT "ltac"; ":"; "("; tac = Pltac.ltac_expr; ")" -> { let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ] ; @@ -402,7 +399,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in - let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in + let t = Tacinterp.hide_interp { Tacinterp.global; ast = t; } in ComTactic.solve g ~info t ~with_end_tac } END @@ -415,7 +412,7 @@ VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof VtProofStep{ proof_block_detection = pbr } } -> { let t, abstract = rm_abstract t in - let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in + let t = Tacinterp.hide_interp { Tacinterp.global = true; ast = t; } in ComTactic.solve_parallel ~info t ~abstract ~with_end_tac } END diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index c186a83a5c..97d75261c5 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -291,7 +291,7 @@ GRAMMAR EXTEND Gram ; simple_intropattern: [ [ pat = simple_intropattern_closed; - l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] -> + l = LIST0 ["%"; c = term LEVEL "0" -> { c } ] -> { let {CAst.loc=loc0;v=pat} = pat in let f c pat = let loc1 = Constrexpr_ops.constr_loc c in @@ -320,7 +320,7 @@ GRAMMAR EXTEND Gram with_bindings: [ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ] ; - red_flags: + red_flag: [ [ IDENT "beta" -> { [FBeta] } | IDENT "iota" -> { [FMatch;FFix;FCofix] } | IDENT "match" -> { [FMatch] } @@ -337,7 +337,7 @@ GRAMMAR EXTEND Gram ] ] ; strategy_flag: - [ [ s = LIST1 red_flags -> { Redops.make_red_flag (List.flatten s) } + [ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) } | d = delta_flag -> { all_with d } ] ] ; @@ -460,7 +460,7 @@ GRAMMAR EXTEND Gram [ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ] ; by_tactic: - [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac } + [ [ "by"; tac = ltac_expr LEVEL "3" -> { Some tac } | -> { None } ] ] ; rewriter : diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index b7b54143df..94e398fe5d 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -37,8 +37,10 @@ let clause_dft_concl = (* Main entries for ltac *) -let tactic_arg = Entry.create "tactic_arg" -let tactic_expr = Entry.create "tactic_expr" +let tactic_value = Entry.create "tactic_value" +let tactic_arg = tactic_value +let ltac_expr = Entry.create "ltac_expr" +let tactic_expr = ltac_expr let binder_tactic = Entry.create "binder_tactic" let tactic = Entry.create "tactic" diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 8565c4b4d6..3a4a081c93 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -31,8 +31,12 @@ val simple_tactic : raw_tactic_expr Entry.t val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t val in_clause : Names.lident Locus.clause_expr Entry.t val clause_dft_concl : Names.lident Locus.clause_expr Entry.t +val tactic_value : raw_tactic_arg Entry.t val tactic_arg : raw_tactic_arg Entry.t + [@@deprecated "Deprecated in 8.13; use 'tactic_value' instead"] +val ltac_expr : raw_tactic_expr Entry.t val tactic_expr : raw_tactic_expr Entry.t + [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"] val binder_tactic : raw_tactic_expr Entry.t val tactic : raw_tactic_expr Entry.t val tactic_eoi : raw_tactic_expr Entry.t diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 6a9fb5c2ea..5e199dad62 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** This module implements pretty-printers for tactic_expr syntactic +(** This module implements pretty-printers for ltac_expr syntactic objects and their subcomponents. *) open Genarg diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 5ef76dbdc1..a1970cbce2 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -769,7 +769,7 @@ let get_rew_prf evars r = match r.rew_prf with let poly_subrelation sort = if sort then PropGlobal.subrelation else TypeGlobal.subrelation -let resolve_subrelation env avoid car rel sort prf rel' res = +let resolve_subrelation env car rel sort prf rel' res = if Termops.eq_constr (fst res.rew_evars) rel rel' then res else let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in @@ -779,7 +779,7 @@ let resolve_subrelation env avoid car rel sort prf rel' res = rew_prf = RewPrf (rel', appsub); rew_evars = evars } -let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) evars = +let resolve_morphism env m args args' (b,cstr) evars = let evars, morph_instance, proj, sigargs, m', args, args' = let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with | Some i -> i @@ -843,18 +843,18 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev let proof = applist (proj, List.rev projargs) in let newt = applist (m', List.rev typeargs) in match respars with - [ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt + [ a, Some r ] -> evars, proof, substl subst a, substl subst r, newt | _ -> assert(false) -let apply_constraint env avoid car rel prf cstr res = +let apply_constraint env car rel prf cstr res = match snd cstr with | None -> res - | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res + | Some r -> resolve_subrelation env car rel (fst cstr) prf r res -let coerce env avoid cstr res = +let coerce env cstr res = let evars, (rel, prf) = get_rew_prf res.rew_evars res in let res = { res with rew_evars = evars } in - apply_constraint env avoid res.rew_car rel prf cstr res + apply_constraint env res.rew_car rel prf cstr res let apply_rule unify loccs : int pure_strategy = let (nowhere_except_in,occs) = convert_occs loccs in @@ -863,7 +863,7 @@ let apply_rule unify loccs : int pure_strategy = then List.mem occ occs else not (List.mem occ occs) in - { strategy = fun { state = occ ; env ; unfresh ; + { strategy = fun { state = occ ; env ; term1 = t ; ty1 = ty ; cstr ; evars } -> let unif = if isEvar (goalevars evars) t then None else unify env evars t in match unif with @@ -874,7 +874,7 @@ let apply_rule unify loccs : int pure_strategy = else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity) else let res = { rew with rew_car = ty } in - let res = Success (coerce env unfresh cstr res) in + let res = Success (coerce env cstr res) in (occ, res) } @@ -968,7 +968,7 @@ let fold_match ?(force=false) env sigma c = let unfold_match env sigma sk app = match EConstr.kind sigma app with - | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> + | App (f', args) when QConstant.equal env (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in Reductionops.whd_beta env sigma (mkApp (v, args)) @@ -1017,10 +1017,10 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | None -> false | Some r -> not (is_rew_cast r.rew_prf)) args' then - let evars', prf, car, rel, c1, c2 = - resolve_morphism env unfresh t m args args' (prop, cstr') evars' + let evars', prf, car, rel, c2 = + resolve_morphism env m args args' (prop, cstr') evars' in - let res = { rew_car = ty; rew_from = c1; + let res = { rew_car = ty; rew_from = t; rew_to = c2; rew_prf = RewPrf (rel, prf); rew_evars = evars' } in Success res @@ -1071,7 +1071,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let res = match prf with | RewPrf (rel, prf) -> - Success (apply_constraint env unfresh res.rew_car + Success (apply_constraint env res.rew_car rel prf (prop,cstr) res) | _ -> Success res in state, res @@ -1094,20 +1094,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Fail | Identity -> res in state, res - (* if x' = None && flags.under_lambdas then *) - (* let lam = mkLambda (n, x, b) in *) - (* let lam', occ = aux env lam occ None in *) - (* let res = *) - (* match lam' with *) - (* | None -> None *) - (* | Some (prf, (car, rel, c1, c2)) -> *) - (* Some (resolve_morphism env sigma t *) - (* ~fnewt:unfold_all *) - (* (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *) - (* cstr evars) *) - (* in res, occ *) - (* else *) - | Prod (n, dom, codom) -> let lam = mkLambda (n, dom, codom) in let (evars', app), unfold = @@ -1131,31 +1117,13 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing dependent relations and using projections to get them out. *) - (* | Lambda (n, t, b) when flags.under_lambdas -> *) - (* let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in *) - (* let n'' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n' in *) - (* let n''' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n'' in *) - (* let rel = new_cstr_evar cstr env (mkApp (Lazy.force coq_relation, [|t|])) in *) - (* let env' = Environ.push_rel_context [(n'',None,lift 2 rel);(n'',None,lift 1 t);(n', None, t)] env in *) - (* let b' = s env' avoid b (Typing.type_of env' (goalevars evars) (lift 2 b)) (unlift_cstr env (goalevars evars) cstr) evars in *) - (* (match b' with *) - (* | Some (Some r) -> *) - (* let prf = match r.rew_prf with *) - (* | RewPrf (rel, prf) -> *) - (* let rel = pointwise_or_dep_relation n' t r.rew_car rel in *) - (* let prf = mkLambda (n', t, prf) in *) - (* RewPrf (rel, prf) *) - (* | x -> x *) - (* in *) - (* Some (Some { r with *) - (* rew_prf = prf; *) - (* rew_car = mkProd (n, t, r.rew_car); *) - (* rew_from = mkLambda(n, t, r.rew_from); *) - (* rew_to = mkLambda (n, t, r.rew_to) }) *) - (* | _ -> b') *) | Lambda (n, t, b) when flags.under_lambdas -> let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in + let unfresh = match n'.binder_name with + | Anonymous -> unfresh + | Name id -> Id.Set.add id unfresh + in let open Context.Rel.Declaration in let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in @@ -1196,7 +1164,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Success r -> let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in let res = make_leibniz_proof env case ty r in - state, Success (coerce env unfresh (prop,cstr) res) + state, Success (coerce env (prop,cstr) res) | Fail | Identity -> if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in @@ -1237,7 +1205,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in let res = match res with - | Success r -> Success (coerce env unfresh (prop,cstr) r) + | Success r -> Success (coerce env (prop,cstr) r) | Fail | Identity -> res in state, res | _ -> state, Fail diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index d58a76fe13..a05b36c1b4 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -31,21 +31,9 @@ type argument = Genarg.ArgT.any Extend.user_symbol (**********************************************************************) (* Interpret entry names of the form "ne_constr_list" as entry keys *) -let coincide s pat off = - let len = String.length pat in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = Char.code s.[off + !i] in - let d = Char.code pat.[!i] in - break := Int.equal c d; - incr i - done; - !break - let atactic n = if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic - else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n) + else Pcoq.Symbol.nterml Pltac.ltac_expr (string_of_int n) type entry_name = EntryName : 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name @@ -70,28 +58,37 @@ let check_separator ?loc = function | Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.") let rec parse_user_entry ?loc s sep = - let l = String.length s in - if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then - let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in + let open CString in + let matches pre suf s = + String.length s > (String.length pre + String.length suf) && + is_prefix pre s && is_suffix suf s + in + let basename pre suf s = + let plen = String.length pre in + String.sub s plen (String.length s - (plen + String.length suf)) + in + let tactic_len = String.length "tactic" in + if matches "ne_" "_list" s then + let entry = parse_user_entry ?loc (basename "ne_" "_list" s) None in check_separator ?loc sep; Ulist1 entry - else if l > 12 && coincide s "ne_" 0 && - coincide s "_list_sep" (l-9) then - let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in + else if matches "ne_" "_list_sep" s then + let entry = parse_user_entry ?loc (basename "ne_" "_list_sep" s) None in Ulist1sep (entry, get_separator sep) - else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in + else if matches "" "_list" s then + let entry = parse_user_entry ?loc (basename "" "_list" s) None in check_separator ?loc sep; Ulist0 entry - else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in + else if matches "" "_list_sep" s then + let entry = parse_user_entry ?loc (basename "" "_list_sep" s) None in Ulist0sep (entry, get_separator sep) - else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in + else if matches "" "_opt" s then + let entry = parse_user_entry ?loc (basename "" "_opt" s) None in check_separator ?loc sep; Uopt entry - else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then - let n = Char.code s.[6] - 48 in + else if String.length s = tactic_len + 1 && is_prefix "tactic" s + && '5' >= s.[tactic_len] && s.[tactic_len] >= '0' then + let n = Char.code s.[tactic_len] - Char.code '0' in check_separator ?loc sep; Uentryl ("tactic", n) else @@ -119,7 +116,7 @@ let get_tactic_entry n = else if Int.equal n 5 then Pltac.binder_tactic, None else if 1<=n && n<5 then - Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n)) + Pltac.ltac_expr, Some (Gramlib.Gramext.Level (string_of_int n)) else user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) @@ -159,7 +156,7 @@ let rec prod_item_of_symbol lev = function EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit)) | Extend.Uentryl (s, n) -> let ArgT.Any tag = s in - assert (coincide (ArgT.repr tag) "tactic" 0); + assert (CString.is_suffix "tactic" (ArgT.repr tag)); get_tacentry n lev (** Tactic grammar extensions *) @@ -386,7 +383,7 @@ let add_ml_tactic_notation name ~level ?deprecation prods = in List.iteri iter (List.rev prods); (* We call [extend_atomic_tactic] only for "basic tactics" (the ones - at tactic_expr level 0) *) + at ltac_expr level 0) *) if Int.equal level 0 then extend_atomic_tactic name prods (**********************************************************************) @@ -423,7 +420,7 @@ let create_ltac_quotation name cast (e, l) = in let action _ v _ _ _ loc = cast (Some loc, v) in let gram = (level, assoc, [Pcoq.Production.make rule action]) in - Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]} + Pcoq.grammar_extend Pltac.tactic_value {pos=None; data=[gram]} (** Command *) @@ -558,10 +555,10 @@ let print_located_tactic qid = let () = let entries = [ - AnyEntry Pltac.tactic_expr; + AnyEntry Pltac.ltac_expr; AnyEntry Pltac.binder_tactic; AnyEntry Pltac.simple_tactic; - AnyEntry Pltac.tactic_arg; + AnyEntry Pltac.tactic_value; ] in register_grammars_by_name "tactic" entries diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 12bfb4d09e..7728415ddd 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1997,7 +1997,7 @@ let interp_tac_gen lfun avoid_ids debug t = let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t (* MUST be marshallable! *) -type tactic_expr = { +type ltac_expr = { global: bool; ast: Tacexpr.raw_tactic_expr; } @@ -2019,7 +2019,7 @@ let hide_interp {global;ast} = hide_interp (Proofview.Goal.env gl) end -let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp +let ComTactic.Interpreter hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp (***************************************************************************) (** Register standard arguments *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 01d7306c9d..fe3079198c 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -126,12 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t -> val interp : raw_tactic_expr -> unit Proofview.tactic (** Hides interpretation for pretty-print *) -type tactic_expr = { +type ltac_expr = { global: bool; ast: Tacexpr.raw_tactic_expr; } -val hide_interp : tactic_expr ComTactic.tactic_interpreter +val hide_interp : ltac_expr -> ComTactic.interpretable (** Internals that can be useful for syntax extensions. *) diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index d464ec4c06..61f90608b1 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -100,7 +100,7 @@ let rec make_form env sigma atom_env term = | Cast(a,_,_) -> make_form env sigma atom_env a | Ind (ind, _) -> - if Names.eq_ind ind (fst (Lazy.force li_False)) then + if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_False)) then Bot else make_atom atom_env (normalize term) @@ -108,11 +108,11 @@ let rec make_form env sigma atom_env term = begin try let ind, _ = destInd sigma hd in - if Names.eq_ind ind (fst (Lazy.force li_and)) then + if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_and)) then let fa = make_form env sigma atom_env argv.(0) in let fb = make_form env sigma atom_env argv.(1) in Conjunct (fa,fb) - else if Names.eq_ind ind (fst (Lazy.force li_or)) then + else if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_or)) then let fa = make_form env sigma atom_env argv.(0) in let fb = make_form env sigma atom_env argv.(1) in Disjunct (fa,fb) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 38b26d06b9..a7ebd5f9f5 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -240,7 +240,7 @@ let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with let same_proj sigma t1 t2 = match EConstr.kind sigma t1, EConstr.kind sigma t2 with - | Proj(c1,_), Proj(c2, _) -> Projection.equal c1 c2 + | Proj(c1,_), Proj(c2, _) -> Projection.CanOrd.equal c1 c2 | _ -> false let all_ok _ _ = true diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index cfdf52a813..35fecfb0a5 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -100,7 +100,7 @@ ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } END GRAMMAR EXTEND Gram GLOBAL: ssrtacarg; - ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]]; + ssrtacarg: [[ tac = ltac_expr LEVEL "5" -> { tac } ]]; END (* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *) @@ -108,7 +108,7 @@ ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } END GRAMMAR EXTEND Gram GLOBAL: ssrtac3arg; - ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]]; + ssrtac3arg: [[ tac = ltac_expr LEVEL "3" -> { tac } ]]; END { @@ -1337,7 +1337,7 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde GRAMMAR EXTEND Gram GLOBAL: ssrbinder; ssrbinder: [ - [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> { + [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> { (FwdPose, [BFvar]), CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ] ]; @@ -1594,18 +1594,18 @@ GRAMMAR EXTEND Gram | n = Prim.natural -> { ArgArg (check_index ~loc n) } ] ]; ssrswap: [[ IDENT "first" -> { loc, true } | IDENT "last" -> { loc, false } ]]; - ssrorelse: [[ "||"; tac = tactic_expr LEVEL "2" -> { tac } ]]; + ssrorelse: [[ "||"; tac = ltac_expr LEVEL "2" -> { tac } ]]; ssrseqarg: [ [ arg = ssrswap -> { noindex, swaptacarg arg } | i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> { i, (tac, def) } | i = ssrseqidx; arg = ssrswap -> { i, swaptacarg arg } - | tac = tactic_expr LEVEL "3" -> { noindex, (mk_hint tac, None) } + | tac = ltac_expr LEVEL "3" -> { noindex, (mk_hint tac, None) } ] ]; END { -let tactic_expr = Pltac.tactic_expr +let ltac_expr = Pltac.ltac_expr } @@ -1688,9 +1688,9 @@ let tclintros_expr ?loc tac ipats = } GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; - tactic_expr: LEVEL "1" [ RIGHTA - [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } + GLOBAL: ltac_expr; + ltac_expr: LEVEL "1" [ RIGHTA + [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } ] ]; END @@ -1704,9 +1704,9 @@ END (* (Removing user-specified parentheses is dubious anyway). *) GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; - ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]]; - tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]]; + GLOBAL: ltac_expr; + ssrparentacarg: [[ "("; tac = ltac_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]]; + ltac_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]]; END (** The internal "done" and "ssrautoprop" tactics. *) @@ -1741,7 +1741,7 @@ let tclBY tac = Tacticals.New.tclTHEN tac (donetac ~-1) (* The latter two are used in forward-chaining tactics (have, suffice, wlog) *) (* and subgoal reordering tacticals (; first & ; last), respectively. *) -(* Force use of the tactic_expr parsing entry, to rule out tick marks. *) +(* Force use of the ltac_expr parsing entry, to rule out tick marks. *) (** The "by" tactical. *) @@ -1782,12 +1782,12 @@ let ssrdotac_expr ?loc n m tac clauses = } GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; + GLOBAL: ltac_expr; ssrdotac: [ - [ tac = tactic_expr LEVEL "3" -> { mk_hint tac } + [ tac = ltac_expr LEVEL "3" -> { mk_hint tac } | tacs = ssrortacarg -> { tacs } ] ]; - tactic_expr: LEVEL "3" [ RIGHTA + ltac_expr: LEVEL "3" [ RIGHTA [ IDENT "do"; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses -> { ssrdotac_expr ~loc noindex m tac clauses } | IDENT "do"; tac = ssrortacarg; clauses = ssrclauses -> @@ -1833,20 +1833,20 @@ let tclseq_expr ?loc tac dir arg = } GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; + GLOBAL: ltac_expr; ssr_first: [ [ tac = ssr_first; ipats = ssrintros_ne -> { tclintros_expr ~loc tac ipats } - | "["; tacl = LIST0 tactic_expr SEP "|"; "]" -> { TacFirst tacl } + | "["; tacl = LIST0 ltac_expr SEP "|"; "]" -> { TacFirst tacl } ] ]; ssr_first_else: [ [ tac1 = ssr_first; tac2 = ssrorelse -> { TacOrelse (tac1, tac2) } | tac = ssr_first -> { tac } ]]; - tactic_expr: LEVEL "4" [ LEFTA - [ tac1 = tactic_expr; ";"; IDENT "first"; tac2 = ssr_first_else -> + ltac_expr: LEVEL "4" [ LEFTA + [ tac1 = ltac_expr; ";"; IDENT "first"; tac2 = ssr_first_else -> { TacThen (tac1, tac2) } - | tac = tactic_expr; ";"; IDENT "first"; arg = ssrseqarg -> + | tac = ltac_expr; ";"; IDENT "first"; arg = ssrseqarg -> { tclseq_expr ~loc tac L2R arg } - | tac = tactic_expr; ";"; IDENT "last"; arg = ssrseqarg -> + | tac = ltac_expr; ";"; IDENT "last"; arg = ssrseqarg -> { tclseq_expr ~loc tac R2L arg } ] ]; END @@ -2448,8 +2448,8 @@ END (* The standard TACTIC EXTEND does not work for abstract *) GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; - tactic_expr: LEVEL "3" + GLOBAL: ltac_expr; + ltac_expr: LEVEL "3" [ RIGHTA [ IDENT "abstract"; gens = ssrdgens -> { ssrtac_expr ~loc "abstract" [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]]; diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 4a907b2795..a49a5e8b28 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -85,7 +85,7 @@ let mk_pat c (na, t) = (c, na, t) GRAMMAR EXTEND Gram GLOBAL: binder_constr; - ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> { mk_rtype t } ]]; + ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]]; ssr_mpat: [[ p = pattern -> { [[p]] } ]]; ssr_dpat: [ [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt } @@ -96,9 +96,9 @@ GRAMMAR EXTEND Gram ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]]; ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]]; binder_constr: [ - [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> + [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) } - | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> + | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> { let b1, ct, rt = db1 in let b1, b2 = let open CAst in let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in @@ -119,7 +119,7 @@ END GRAMMAR EXTEND Gram GLOBAL: closed_binder; closed_binder: [ - [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> + [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> { [CLocalAssum ([CAst.make ~loc Anonymous], Default Explicit, c)] } ] ]; END @@ -309,9 +309,15 @@ END ~category:"deprecated" ~default:CWarnings.Enabled (fun () -> (Pp.strbrk - "SSReflect's Search command has been moved to the \ - ssrsearch module; please Require that module if you \ - still want to use SSReflect's Search command")) + "In previous versions of Coq, loading SSReflect had the effect of \ + replacing the built-in 'Search' command with an SSReflect version \ + of that command. \ + Coq's own search feature was still available via 'SearchAbout' \ + (but that alias is deprecated). \ + This replacement no longer happens; now 'Search' calls Coq's own search \ + feature even when SSReflect is loaded. \ + If you want to use SSReflect's deprecated Search command \ + instead of the built-in one, please Require the ssrsearch module.")) open G_vernac } diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index cdd15acb0d..bd514f15d5 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -463,8 +463,8 @@ let nb_cs_proj_args pc f u = try match kind f with | Prod _ -> na Prod_cs | Sort s -> na (Sort_cs (Sorts.family s)) - | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f - | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f + | Const (c',_) when Constant.CanOrd.equal c' pc -> nargs_of_proj u.up_f + | Proj (c',_) when Constant.CanOrd.equal (Projection.constant c') pc -> nargs_of_proj u.up_f | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f)) | _ -> -1 with Not_found -> -1 @@ -508,7 +508,7 @@ let filter_upat i0 f n u fpats = let () = if !i0 < np then i0 := n in (u, np) :: fpats let eq_prim_proj c t = match kind t with - | Proj(p,_) -> Constant.equal (Projection.constant p) c + | Proj(p,_) -> Constant.CanOrd.equal (Projection.constant p) c | _ -> false let filter_upat_FO i0 f n u fpats = diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index c030925ea9..93d91abea3 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -31,7 +31,7 @@ let warn_deprecated_numeral_notation = } -VERNAC ARGUMENT EXTEND numnotoption +VERNAC ARGUMENT EXTEND numeral_modifier PRINTED BY { pr_numnot_option } | [ ] -> { Nop } | [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) } @@ -40,11 +40,11 @@ END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) numnotoption(o) ] -> + ident(sc) numeral_modifier(o) ] -> { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) numnotoption(o) ] -> + ident(sc) numeral_modifier(o) ] -> { warn_deprecated_numeral_notation (); vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } |