diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extraargs.ml4 | 4 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 69 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.ml4 | 23 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 18 | ||||
| -rw-r--r-- | plugins/ltac/g_obligations.ml4 | 12 | ||||
| -rw-r--r-- | plugins/ltac/g_rewrite.ml4 | 39 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 58 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 15 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 7 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 7 |
11 files changed, 160 insertions, 94 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 89feea8dcf..bb01aca558 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -133,7 +133,9 @@ let pr_occurrences = pr_occurrences () () () let pr_gen prc _prlc _prtac c = prc c -let pr_globc _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr glob +let pr_globc _prc _prlc _prtac (_,glob) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env glob let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 4b1555e551..982fc7cc3c 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -313,30 +313,51 @@ let project_hint pri l2r r = let id = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in - let ctx = Evd.universe_context_set sigma in + let poly = Flags.use_polymorphic_flag () in + let ctx = Evd.const_univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) -let add_hints_iff l2r lc n bl = - let l = Locality.LocalityFixme.consume () in - Hints.add_hints (Locality.make_module_locality l) bl +let add_hints_iff ?locality l2r lc n bl = + Hints.add_hints (Locality.make_module_locality locality) bl (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc)) -VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> - [ add_hints_iff true lc n bl ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality true lc n bl; + st + end + ] | [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] -> - [ add_hints_iff true lc n ["core"] ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality true lc n ["core"]; + st + end + ] END -VERNAC COMMAND EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF + +VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> - [ add_hints_iff false lc n bl ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality false lc n bl; + st + end + ] | [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] -> - [ add_hints_iff false lc n ["core"] ] + [ fun ~atts ~st -> begin + let open Vernacinterp in + add_hints_iff ?locality:atts.locality false lc n ["core"]; + st + end + ] END (**********************************************************************) @@ -852,34 +873,12 @@ TACTIC EXTEND is_evar ] END -let has_evar sigma c = -let rec has_evar x = - match EConstr.kind sigma x with - | Evar _ -> true - | Rel _ | Var _ | Meta _ | Sort _ | Const _ | Ind _ | Construct _ -> - false - | Cast (t1, _, t2) | Prod (_, t1, t2) | Lambda (_, t1, t2) -> - has_evar t1 || has_evar t2 - | LetIn (_, t1, t2, t3) -> - has_evar t1 || has_evar t2 || has_evar t3 - | App (t1, ts) -> - has_evar t1 || has_evar_array ts - | Case (_, t1, t2, ts) -> - has_evar t1 || has_evar t2 || has_evar_array ts - | Fix ((_, tr)) | CoFix ((_, tr)) -> - has_evar_prec tr - | Proj (p, c) -> has_evar c -and has_evar_array x = - Array.exists has_evar x -and has_evar_prec (_, ts1, ts2) = - Array.exists has_evar ts1 || Array.exists has_evar ts2 -in -has_evar c - TACTIC EXTEND has_evar | [ "has_evar" constr(x) ] -> [ Proofview.tclEVARMAP >>= fun sigma -> - if has_evar sigma x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars") + if Evarutil.has_undefined_evars sigma x + then Proofview.tclUNIT () + else Tacticals.New.tclFAIL 0 (str "No evars") ] END diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 5baa0d5c1d..90a44708fc 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -51,8 +51,12 @@ let eval_uconstrs ist cs = List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr -let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c) -let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob +let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env c) +let pr_auto_using _ _ _ = Pptactic.pr_auto_using + (let sigma, env = Pfedit.get_current_context () in + Printer.pr_closed_glob_env env sigma) ARGUMENT EXTEND auto_using TYPED AS uconstr_list @@ -186,7 +190,7 @@ END let pr_hints_path prc prx pry c = Hints.pp_hints_path c let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c let glob_hints_path ist = Hints.glob_hints_path - + ARGUMENT EXTEND hints_path PRINTED BY pr_hints_path @@ -210,10 +214,15 @@ ARGUMENT EXTEND opthints | [ ] -> [ None ] END -VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ - let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (match dbnames with None -> ["core"] | Some l -> l) entry ] + fun ~atts ~st -> begin + let open Vernacinterp in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in + Hints.add_hints (Locality.make_section_locality atts.locality) + (match dbnames with None -> ["core"] | Some l -> l) entry; + st + end + ] END diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 1161525689..34fea6175b 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -469,13 +469,13 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ] END -VERNAC COMMAND EXTEND VernacTacticNotation +VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => [ VtUnknown, VtNow ] -> - [ - let l = Locality.LocalityFixme.consume () in - let n = Option.default 0 n in - Tacentries.add_tactic_notation (Locality.make_module_locality l) n r e + [ fun ~atts ~st -> let open Vernacinterp in + let n = Option.default 0 n in + Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; + st ] END @@ -512,15 +512,15 @@ PRINTED BY pr_tacdef_body | [ tacdef_body(t) ] -> [ t ] END -VERNAC COMMAND EXTEND VernacDeclareTacticDefinition +VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function | TacticDefinition ((_,r),_) -> r | TacticRedefinition (Ident (_,r),_) -> r | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater - ] -> [ - let lc = Locality.LocalityFixme.consume () in - Tacentries.register_ltac (Locality.make_module_locality lc) l + ] -> [ fun ~atts ~st -> let open Vernacinterp in + Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; + st ] END diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index fea9e837b1..f6cc3833a7 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -123,11 +123,15 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF | [ "Admit" "Obligations" ] -> [ admit_obligations None ] END -VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND Set_Solver CLASSIFIED AS SIDEFF | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - set_default_tactic - (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (Tacintern.glob_tactic t) ] + fun ~atts ~st -> begin + let open Vernacinterp in + set_default_tactic + (Locality.make_section_locality atts.locality) + (Tacintern.glob_tactic t); + st + end] END open Pp diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b148d962ed..ea1808a255 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -31,8 +31,12 @@ type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings -let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = Printer.pr_glob_constr (fst (fst (snd ge))) -let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge)) +let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env (fst (fst (snd ge))) +let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env (fst (fst ge)) let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge) let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c) let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l @@ -239,22 +243,37 @@ VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] END -VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF +VERNAC COMMAND FUNCTIONAL EXTEND AddSetoid1 CLASSIFIED AS SIDEFF [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] a aeq t n ] + [ fun ~atts ~st -> let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n; + st + ] | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders a aeq t n ] + [ fun ~atts ~st -> let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n; + st + ] | [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ] - -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n; + st + ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n; + st + ] | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ] + -> [ fun ~atts ~st -> let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n; + st + ] END TACTIC EXTEND setoid_symmetry @@ -272,5 +291,7 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY - [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) ] + [ "Print" "Rewrite" "HintDb" preident(s) ] -> + [ let sigma, env = Pfedit.get_current_context () in + Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) ] END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 38460c669f..d707512457 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -84,6 +84,14 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +let string_of_genarg_arg (ArgumentType arg) = + let rec aux : type a b c. (a, b, c) genarg_type -> string = function + | ListArg t -> aux t ^ "_list" + | OptArg t -> aux t ^ "_opt" + | PairArg (t1, t2) -> assert false (* No parsing/printing rule for it *) + | ExtraArg s -> ArgT.repr s in + aux arg + let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) @@ -536,15 +544,24 @@ let pr_goal_selector ~toplevel s = let pr_funvar n = spc () ++ Name.print n - let pr_let_clause k pr (na,(bl,t)) = + let pr_let_clause k pr_gen pr_arg (na,(bl,t)) = + let pr = function + | TacGeneric arg -> + let name = string_of_genarg_arg (genarg_tag arg) in + if name = "unit" || name = "int" then + (* Hard-wired parsing rules *) + pr_gen arg + else + str name ++ str ":" ++ surround (pr_gen arg) + | _ -> pr_arg (TacArg (Loc.tag t)) in hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ - str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t))) + str " :=" ++ brk (1,1) ++ pr t) - let pr_let_clauses recflag pr = function + let pr_let_clauses recflag pr_gen pr = function | hd::tl -> hv 0 - (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ - prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) + (pr_let_clause (if recflag then "let rec" else "let") pr_gen pr hd ++ + prlist (fun t -> spc () ++ pr_let_clause "with" pr_gen pr t) tl) | [] -> anomaly (Pp.str "LetIn must declare at least one binding.") let pr_seq_body pr tl = @@ -858,7 +875,7 @@ let pr_goal_selector ~toplevel s = let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in v 0 (hv 0 ( - pr_let_clauses recflag (pr_tac ltop) llc + pr_let_clauses recflag pr.pr_generic (pr_tac ltop) llc ++ spc () ++ keyword "in" ) ++ fnl () ++ pr_tac (llet,E) u), llet @@ -1003,7 +1020,7 @@ let pr_goal_selector ~toplevel s = | TacAtom (loc,t) -> pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom | TacArg(_,Tacexp e) -> - pr.pr_tactic (latom,E) e, latom + pr_tac inherited e, latom | TacArg(_,ConstrMayEval (ConstrTerm c)) -> keyword "constr:" ++ pr.pr_constr c, latom | TacArg(_,ConstrMayEval c) -> @@ -1226,6 +1243,15 @@ let make_constr_printer f c = let lift f a = Genprint.PrinterBasic (fun () -> f a) + +let pr_glob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_glob_constr_env env c + +let pr_lglob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_lglob_constr_env env c + let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in @@ -1240,7 +1266,7 @@ let () = Genprint.register_print0 wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) - (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) + (Miscprint.pr_intro_pattern (fun (c, _) -> pr_glob_constr_pptac c)) pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl @@ -1251,45 +1277,45 @@ let () = Genprint.register_print0 wit_constr Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr Ppconstr.pr_constr_expr - (fun (c,_) -> Printer.pr_glob_constr c) + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_red_expr (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) - (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) + (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)) pr_red_expr_env ; Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); Genprint.register_print0 wit_bindings (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_bindings_env ; Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_with_bindings_env ; Genprint.register_print0 wit_open_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_with_bindings_env ; Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) - (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_destruction_arg_env ; Genprint.register_print0 Stdarg.wit_int int int (lift int); diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 705a51edd3..c0060c5a7c 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Pp open CErrors open Util +open Names open Nameops open Namegen open Constr @@ -1143,7 +1143,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = (* | _ -> b') *) | Lambda (n, t, b) when flags.under_lambdas -> - let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in + let n' = Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env) n 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 @@ -1800,9 +1800,9 @@ let declare_instance_trans global binders a aeq n lemma = in anew_instance global binders instance [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)] -let declare_relation ?(binders=[]) a aeq n refl symm trans = +let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = init_setoid (); - let global = not (Locality.make_section_locality (Locality.LocalityFixme.consume ())) in + let global = not (Locality.make_section_locality locality) in let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in ignore(anew_instance global binders instance []); match (refl,symm,trans) with @@ -1884,11 +1884,11 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in + let univs = Evd.const_univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = - Declare.definition_entry ~types:typ ~poly ~univs:ctx term + Declare.definition_entry ~types:typ ~univs term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) @@ -1972,9 +1972,10 @@ let add_morphism_infer glob m n = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then + let uctx = UState.const_univ_entry ~poly uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry - (None,poly,(instance,UState.context uctx),None), + (None,(instance,uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 1306c590ba..17e7244b39 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -75,7 +75,7 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : +val declare_relation : ?locality:bool -> ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> constr_expr option -> constr_expr option -> constr_expr option -> unit diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 180fb2db40..918d1faebe 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -91,9 +91,10 @@ let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in if not (is_global ref' t') then - Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ - str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ - pr_global ref') ; + (let sigma, env = Pfedit.get_current_context () in + Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ + str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++ + pr_global ref')); ref' in subst_or_var (subst_located subst_global) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index a669692fc9..2dd7c9a747 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -20,7 +20,9 @@ let prmatchpatt env sigma hyp = Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp let prmatchrl rl = Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env())) - (fun (_,p) -> Printer.pr_constr_pattern p) rl + (fun (_,p) -> + let sigma, env = Pfedit.get_current_context () in + Printer.pr_constr_pattern_env env sigma p) rl (* This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more @@ -369,7 +371,8 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) + let sigma, env = Pfedit.get_current_context () in + Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) in |