aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/setoid_ring/ArithRing.v2
-rw-r--r--contrib/setoid_ring/InitialRing.v30
-rw-r--r--contrib/setoid_ring/NArithRing.v2
-rw-r--r--contrib/setoid_ring/Ring.v2
-rw-r--r--contrib/setoid_ring/ZArithRing.v8
-rw-r--r--parsing/g_ltac.ml414
-rw-r--r--parsing/pptactic.ml1
-rw-r--r--tactics/tacinterp.ml109
-rw-r--r--test-suite/success/ltac.v13
9 files changed, 115 insertions, 66 deletions
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
index 074f6ef79..601cabe00 100644
--- a/contrib/setoid_ring/ArithRing.v
+++ b/contrib/setoid_ring/ArithRing.v
@@ -32,7 +32,7 @@ Qed.
Ltac natcst t :=
match isnatcst t with
true => constr:(N_of_nat t)
- | _ => InitialRing.NotConstant
+ | _ => constr:InitialRing.NotConstant
end.
Ltac Ss_to_add f acc :=
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index 4d96bec4c..c1fa963f2 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -667,17 +667,17 @@ End GEN_DIV.
| (add rI (add rI rI)) => constr:3%positive
| (mul (add rI rI) ?p) => (* 2p *)
match inv_cst p with
- NotConstant => NotConstant
- | 1%positive => NotConstant (* 2*1 is not convertible to 2 *)
+ NotConstant => constr:NotConstant
+ | 1%positive => constr:NotConstant (* 2*1 is not convertible to 2 *)
| ?p => constr:(xO p)
end
| (add rI (mul (add rI rI) ?p)) => (* 1+2p *)
match inv_cst p with
- NotConstant => NotConstant
- | 1%positive => NotConstant
+ NotConstant => constr:NotConstant
+ | 1%positive => constr:NotConstant
| ?p => constr:(xI p)
end
- | _ => NotConstant
+ | _ => constr:NotConstant
end in
inv_cst t.
@@ -687,7 +687,7 @@ End GEN_DIV.
rO => constr:NwO
| _ =>
match inv_gen_phi_pos rI add mul t with
- NotConstant => NotConstant
+ NotConstant => constr:NotConstant
| ?p => constr:(Npos p::nil)
end
end.
@@ -699,7 +699,7 @@ End GEN_DIV.
rO => constr:0%N
| _ =>
match inv_gen_phi_pos rI add mul t with
- NotConstant => NotConstant
+ NotConstant => constr:NotConstant
| ?p => constr:(Npos p)
end
end.
@@ -710,12 +710,12 @@ End GEN_DIV.
rO => constr:0%Z
| (opp ?p) =>
match inv_gen_phi_pos rI add mul p with
- NotConstant => NotConstant
+ NotConstant => constr:NotConstant
| ?p => constr:(Zneg p)
end
| _ =>
match inv_gen_phi_pos rI add mul t with
- NotConstant => NotConstant
+ NotConstant => constr:NotConstant
| ?p => constr:(Zpos p)
end
end.
@@ -731,7 +731,7 @@ Ltac inv_gen_phi rO rI cO cI t :=
end.
(* A simple tactic recognizing no constant *)
- Ltac inv_morph_nothing t := constr:(NotConstant).
+ Ltac inv_morph_nothing t := constr:NotConstant.
Ltac coerce_to_almost_ring set ext rspec :=
match type of rspec with
@@ -875,9 +875,9 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk :=
(* Tactic for constant *)
Ltac isnatcst t :=
match t with
- O => true
+ O => constr:true
| S ?p => isnatcst p
- | _ => false
+ | _ => constr:false
end.
Ltac isPcst t :=
@@ -887,7 +887,7 @@ Ltac isPcst t :=
| xH => constr:true
(* nat -> positive *)
| P_of_succ_nat ?n => isnatcst n
- | _ => false
+ | _ => constr:false
end.
Ltac isNcst t :=
@@ -899,7 +899,7 @@ Ltac isNcst t :=
Ltac isZcst t :=
match t with
- Z0 => true
+ Z0 => constr:true
| Zpos ?p => isPcst p
| Zneg ?p => isPcst p
(* injection nat -> Z *)
@@ -907,7 +907,7 @@ Ltac isZcst t :=
(* injection N -> Z *)
| Z_of_N ?n => isNcst n
(* *)
- | _ => false
+ | _ => constr:false
end.
diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v
index ae067a8a2..0ba519fde 100644
--- a/contrib/setoid_ring/NArithRing.v
+++ b/contrib/setoid_ring/NArithRing.v
@@ -15,7 +15,7 @@ Set Implicit Arguments.
Ltac Ncst t :=
match isNcst t with
true => t
- | _ => NotConstant
+ | _ => constr:NotConstant
end.
Add Ring Nr : Nth (decidable Neq_bool_ok, constants [Ncst]).
diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v
index 1a4e1cc75..d01b16258 100644
--- a/contrib/setoid_ring/Ring.v
+++ b/contrib/setoid_ring/Ring.v
@@ -38,7 +38,7 @@ Ltac bool_cst t :=
match t with
true => constr:true
| false => constr:false
- | _ => NotConstant
+ | _ => constr:NotConstant
end.
Add Ring bool_ring : BoolTheory (decidable bool_eq_ok, constants [bool_cst]).
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 3cdce8da4..4a5b623b4 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -17,14 +17,14 @@ Set Implicit Arguments.
Ltac Zcst t :=
match isZcst t with
true => t
- | _ => NotConstant
+ | _ => constr:NotConstant
end.
Ltac isZpow_coef t :=
match t with
| Zpos ?p => isPcst p
- | Z0 => true
- | _ => false
+ | Z0 => constr:true
+ | _ => constr:false
end.
Definition N_of_Z x :=
@@ -36,7 +36,7 @@ Definition N_of_Z x :=
Ltac Zpow_tac t :=
match isZpow_coef t with
| true => constr:(N_of_Z t)
- | _ => constr:(NotConstant)
+ | _ => constr:NotConstant
end.
Ltac Zpower_neg :=
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index f7a538720..eefbe7da0 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -25,11 +25,6 @@ let fail_default_value = ArgArg 0
let arg_of_expr = function
TacArg a -> a
| e -> Tacexp (e:raw_tactic_expr)
-
-let tacarg_of_expr = function
- | TacArg (Reference r) -> TacCall (dummy_loc,r,[])
- | TacArg a -> a
- | e -> Tacexp (e:raw_tactic_expr)
(* Tactics grammar rules *)
@@ -101,9 +96,8 @@ GEXTEND Gram
TacArg(ConstrMayEval(ConstrTerm c))
| IDENT "ipattern"; ":"; ipat = simple_intropattern ->
TacArg(IntroPattern ipat)
- | r = reference; la = LIST1 tactic_arg ->
- TacArg(TacCall (loc,r,la))
- | r = reference -> TacArg (Reference r) ]
+ | r = reference; la = LIST0 tactic_arg ->
+ TacArg(TacCall (loc,r,la)) ]
| "0"
[ "("; a = tactic_expr; ")" -> a
| a = tactic_atom -> TacArg a ] ]
@@ -120,7 +114,7 @@ GEXTEND Gram
;
(* Tactic arguments *)
tactic_arg:
- [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> tacarg_of_expr a
+ [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a
| IDENT "ltac"; ":"; n = natural -> Integer n
| IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat
| a = may_eval_arg -> a
@@ -152,7 +146,7 @@ GEXTEND Gram
tactic_atom:
[ [ id = METAIDENT -> MetaIdArg (loc,true,id)
| n = integer -> Integer n
- | r = reference -> Reference r
+ | r = reference -> TacCall (loc,r,[])
| "()" -> TacVoid ] ]
;
match_key:
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d4befac1e..57f1e80bd 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -946,6 +946,7 @@ let rec pr_tac inherited tac =
pr_may_eval pr_constr pr_lconstr pr_cst c, leval
| TacArg(TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom
| TacArg(Integer n) -> int n, latom
+ | TacArg(TacCall(loc,f,[])) -> pr_ref f, latom
| TacArg(TacCall(loc,f,l)) ->
pr_with_comments loc
(hov 1 (pr_ref f ++ spc () ++
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 068ae8e96..c9dee28d2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -59,6 +59,8 @@ let error_syntactic_metavariables_not_allowed loc =
(loc,"out_ident",
str "Syntactic metavariables allowed only in quotations")
+let error_global_not_found_loc (loc,qid) = error_global_not_found_loc loc qid
+
let skip_metaid = function
| AI x -> x
| MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc
@@ -234,10 +236,9 @@ let _ =
]
let lookup_atomic id = Idmap.find id !atomic_mactab
-let is_atomic id = Idmap.mem id !atomic_mactab
let is_atomic_kn kn =
let (_,_,l) = repr_kn kn in
- is_atomic (id_of_label l)
+ Idmap.mem (id_of_label l) !atomic_mactab
(* Summary and Object declaration *)
let mactab = ref Gmap.empty
@@ -398,26 +399,21 @@ let intern_inductive ist = function
let intern_global_reference ist = function
| Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
| r ->
- let loc,qid as lqid = qualid_of_reference r in
+ let loc,_ as lqid = qualid_of_reference r in
try ArgArg (loc,locate_global_with_alias lqid)
with Not_found ->
- error_global_not_found_loc loc qid
+ error_global_not_found_loc lqid
-let intern_tac_ref ist = function
- | Ident (loc,id) when find_ltacvar id ist -> ArgVar (loc,id)
+let intern_ltac_variable ist = function
| Ident (loc,id) ->
- ArgArg (loc,
- try find_recvar id ist
- with Not_found -> locate_tactic (make_short_qualid id))
- | r ->
- let (loc,qid) = qualid_of_reference r in
- ArgArg (loc,locate_tactic qid)
-
-let intern_tactic_reference ist r =
- try intern_tac_ref ist r
- with Not_found ->
- let (loc,qid) = qualid_of_reference r in
- error_global_not_found_loc loc qid
+ if find_ltacvar id ist then
+ (* A local variable of any type *)
+ ArgVar (loc,id)
+ else
+ (* A recursive variable *)
+ ArgArg (loc,find_recvar id ist)
+ | _ ->
+ raise Not_found
let intern_constr_reference strict ist = function
| Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist ->
@@ -426,17 +422,63 @@ let intern_constr_reference strict ist = function
let loc,_ as lqid = qualid_of_reference r in
RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r)
-let intern_reference strict ist r =
- (try Reference (intern_tac_ref ist r)
- with Not_found ->
- (try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
- with Not_found ->
- (match r with
- | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id)
- | Ident (loc,id) when not strict -> IntroPattern (IntroIdentifier id)
- | _ ->
- let (loc,qid) = qualid_of_reference r in
- error_global_not_found_loc loc qid)))
+(* Internalize an isolated reference in position of tactic *)
+
+let intern_isolated_global_tactic_reference r =
+ let (loc,qid) = qualid_of_reference r in
+ try TacCall (loc,ArgArg (loc,locate_tactic qid),[])
+ with Not_found ->
+ match r with
+ | Ident (_,id) -> Tacexp (lookup_atomic id)
+ | _ -> raise Not_found
+
+let intern_isolated_tactic_reference ist r =
+ (* An ltac reference *)
+ try Reference (intern_ltac_variable ist r)
+ with Not_found ->
+ (* A global tactic *)
+ try intern_isolated_global_tactic_reference r
+ with Not_found ->
+ (* Tolerance for compatibility, allow not to use "constr:" *)
+ try ConstrMayEval (ConstrTerm (intern_constr_reference true ist r))
+ with Not_found ->
+ (* Reference not found *)
+ error_global_not_found_loc (qualid_of_reference r)
+
+(* Internalize an applied tactic reference *)
+
+let intern_applied_global_tactic_reference r =
+ let (loc,qid) = qualid_of_reference r in
+ ArgArg (loc,locate_tactic qid)
+
+let intern_applied_tactic_reference ist r =
+ (* An ltac reference *)
+ try intern_ltac_variable ist r
+ with Not_found ->
+ (* A global tactic *)
+ try intern_applied_global_tactic_reference r
+ with Not_found ->
+ (* Reference not found *)
+ error_global_not_found_loc (qualid_of_reference r)
+
+(* Intern a reference parsed in a non-tactic entry *)
+
+let intern_non_tactic_reference strict ist r =
+ (* An ltac reference *)
+ try Reference (intern_ltac_variable ist r)
+ with Not_found ->
+ (* A constr reference *)
+ try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
+ with Not_found ->
+ (* Tolerance for compatibility, allow not to use "ltac:" *)
+ try intern_isolated_global_tactic_reference r
+ with Not_found ->
+ (* By convention, use IntroIdentifier for unbound ident, when not in a def *)
+ match r with
+ | Ident (_,id) when not strict -> IntroPattern (IntroIdentifier id)
+ | _ ->
+ (* Reference not found *)
+ error_global_not_found_loc (qualid_of_reference r)
let intern_message_token ist = function
| (MsgString _ | MsgInt _ as x) -> x
@@ -515,12 +557,12 @@ let short_name = function
| _ -> None
let interp_global_reference r =
- let loc,qid as lqid = qualid_of_reference r in
+ let lqid = qualid_of_reference r in
try locate_global_with_alias lqid
with Not_found ->
match r with
| Ident (loc,id) when not !strict_check -> VarRef id
- | _ -> error_global_not_found_loc loc qid
+ | _ -> error_global_not_found_loc lqid
let intern_evaluable_reference_or_by_notation = function
| AN r -> evaluable_of_global_reference (interp_global_reference r)
@@ -823,7 +865,7 @@ and intern_tactic_fun ist (var,body) =
and intern_tacarg strict ist = function
| TacVoid -> TacVoid
- | Reference r -> intern_reference strict ist r
+ | Reference r -> intern_non_tactic_reference strict ist r
| IntroPattern ipat ->
let lf = ref([],[]) in (*How to know what names the intropattern binds?*)
IntroPattern (intern_intro_pattern lf ist ipat)
@@ -836,9 +878,10 @@ and intern_tacarg strict ist = function
if istac then Reference (ArgVar (adjust_loc loc,id))
else ConstrMayEval (ConstrTerm (RVar (adjust_loc loc,id), None))
else error_syntactic_metavariables_not_allowed loc
+ | TacCall (loc,f,[]) -> intern_isolated_tactic_reference ist f
| TacCall (loc,f,l) ->
TacCall (loc,
- intern_tactic_reference ist f,
+ intern_applied_tactic_reference ist f,
List.map (intern_tacarg !strict_check ist) l)
| TacExternal (loc,com,req,la) ->
TacExternal (loc,com,req,List.map (intern_tacarg !strict_check ist) la)
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 9dd7b273d..757cf6a4e 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -173,7 +173,7 @@ Abort.
empty args *)
Goal True.
-match None with @None => exact I end.
+match constr:@None with @None => exact I end.
Abort.
(* Check second-order pattern unification *)
@@ -209,3 +209,14 @@ Goal True -> True -> True.
is.
exact I.
Abort.
+
+(* Interférence entre espaces des noms *)
+
+Ltac O := intro.
+Ltac Z1 t := set (x:=t).
+Ltac Z2 t := t.
+Goal True -> True.
+Z1 O.
+Z2 ltac:O.
+exact I.
+Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 22:20:44 +0000