aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml469
-rw-r--r--plugins/ltac/g_auto.ml415
-rw-r--r--plugins/ltac/g_ltac.ml418
-rw-r--r--plugins/ltac/g_obligations.ml412
-rw-r--r--plugins/ltac/g_rewrite.ml427
-rw-r--r--plugins/ltac/rewrite.ml11
-rw-r--r--plugins/ltac/rewrite.mli2
-rw-r--r--plugins/ltac/tacinterp.ml39
8 files changed, 121 insertions, 72 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 4b1555e55..982fc7cc3 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 84e79d8ab..90a44708f 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -190,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
@@ -214,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 116152568..34fea6175 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 fea9e837b..f6cc3833a 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 91abe1019..ea1808a25 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -243,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
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c63492d1b..c0060c5a7 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -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 1306c590b..17e7244b3 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/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 1a8ec6d6f..14b79d73e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1380,13 +1380,38 @@ and tactic_of_value ist vle =
extra = TacStore.set ist.extra f_trace []; } in
let tac = name_if_glob appl (eval_tactic ist t) in
Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
- | VFun (_, _, _,vars,_) ->
- let numargs = List.length vars in
- Tacticals.New.tclZEROMSG
- (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++
- Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++
- Pp.str (String.plural numargs "variable") ++ Pp.str " " ++
- pr_enum Name.print vars ++ Pp.str ".")
+ | VFun (appl,_,vmap,vars,_) ->
+ let tactic_nm =
+ match appl with
+ UnnamedAppl -> "An unnamed user-defined tactic"
+ | GlbAppl apps ->
+ let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in
+ match nms with
+ [] -> assert false
+ | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *)
+ in
+ let numargs = List.length vars in
+ let givenargs =
+ List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in
+ let numgiven = List.length givenargs in
+ Tacticals.New.tclZEROMSG
+ (Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++
+ (match numargs with
+ 0 -> assert false
+ | 1 ->
+ Pp.str "There is a missing argument for variable " ++
+ (Name.print (List.hd vars))
+ | _ -> Pp.str "There are missing arguments for variables " ++
+ pr_enum Name.print vars) ++ Pp.pr_comma () ++
+ match numgiven with
+ 0 ->
+ Pp.str "no arguments at all were provided."
+ | 1 ->
+ Pp.str "an argument was provided for variable " ++
+ Pp.str (List.hd givenargs) ++ Pp.str "."
+ | _ ->
+ Pp.str "arguments were provided for variables " ++
+ pr_enum Pp.str givenargs ++ Pp.str ".")
| VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
else if has_type vle (topwit wit_tactic) then
let tac = out_gen (topwit wit_tactic) vle in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 05:24:25 +0000