aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml2
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile2
-rw-r--r--doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst5
-rw-r--r--doc/sphinx/proof-engine/ltac2.rst5
-rw-r--r--tactics/hipattern.ml53
-rw-r--r--test-suite/bugs/closed/bug_12806.v9
-rw-r--r--user-contrib/Ltac2/tac2core.ml11
-rw-r--r--user-contrib/Ltac2/tac2quote.ml18
-rw-r--r--user-contrib/Ltac2/tac2quote.mli2
-rw-r--r--vernac/record.ml4
10 files changed, 70 insertions, 41 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 19ee32dd84..52b03e455b 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -20,7 +20,7 @@ variables:
# Format: $IMAGE-V$DATE-$hash
# The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
# echo $(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10)
- CACHEKEY: "bionic_coq-V2021-04-14-4d961e49fc"
+ CACHEKEY: "bionic_coq-V2021-04-14-802aebab96"
IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
# By default, jobs run in the base switch; override to select another switch
OPAM_SWITCH: "base"
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index b90457add7..00729cd168 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -24,7 +24,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
texlive-science tipa
# More dependencies of the sphinx doc, pytest for coqtail
-RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \
+RUN pip3 install docutils==0.16 sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \
antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 \
pytest==5.4.3
diff --git a/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst
new file mode 100644
index 0000000000..9753ce915b
--- /dev/null
+++ b/doc/changelog/05-tactic-language/13939-ltac2-open-constr-scope.rst
@@ -0,0 +1,5 @@
+- **Added:**
+ Allow scope delimiters in Ltac2 open_constr:(...) quotation
+ (`#13939 <https://github.com/coq/coq/pull/13939>`_,
+ fixes `#12806 <https://github.com/coq/coq/issues/12806>`_,
+ by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 294c56ef06..25ac72069b 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1375,8 +1375,9 @@ table further down lists the classes that that are handled plainly.
the term (as described in :ref:`LocalInterpretationRulesForNotations`). The last
:token:`scope_key` is the top of the scope stack that's applied to the :token:`term`.
- :n:`open_constr`
- Parses an open :token:`term`.
+ :n:`open_constr {? ( {+, @scope_key } ) }`
+ Parses an open :token:`term`. Like :n:`constr` above, this class
+ accepts a list of notation scopes with the same effects.
:n:`ident`
Parses :token:`ident` or :n:`$@ident`. The first form returns :n:`ident:(@ident)`,
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 5338e0eef5..783a317b3a 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -293,31 +293,34 @@ let match_with_equation env sigma t =
let (hdapp,args) = destApp sigma t in
match EConstr.kind sigma hdapp with
| Ind (ind,u) ->
- if Coqlib.check_ind_ref "core.eq.type" ind then
- Some (build_coq_eq_data()),hdapp,
- PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if Coqlib.check_ind_ref "core.identity.type" ind then
- Some (build_coq_identity_data()),hdapp,
- PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if Coqlib.check_ind_ref "core.JMeq.type" ind then
- Some (build_coq_jmeq_data()),hdapp,
- HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
- else
- let (mib,mip) = Global.lookup_inductive ind in
- let constr_types = mip.mind_nf_lc in
- let nconstr = Array.length mip.mind_consnames in
- if Int.equal nconstr 1 then
- let (ctx, cty) = constr_types.(0) in
- let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
- if is_matching env sigma coq_refl_leibniz1_pattern cty then
- None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
- else if is_matching env sigma coq_refl_leibniz2_pattern cty then
- None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if is_matching env sigma coq_refl_jm_pattern cty then
- None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
- else raise NoEquationFound
- else raise NoEquationFound
- | _ -> raise NoEquationFound
+ (try
+ if Coqlib.check_ind_ref "core.eq.type" ind then
+ Some (build_coq_eq_data()),hdapp,
+ PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+ else if Coqlib.check_ind_ref "core.identity.type" ind then
+ Some (build_coq_identity_data()),hdapp,
+ PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+ else if Coqlib.check_ind_ref "core.JMeq.type" ind then
+ Some (build_coq_jmeq_data()),hdapp,
+ HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
+ else
+ let (mib,mip) = Global.lookup_inductive ind in
+ let constr_types = mip.mind_nf_lc in
+ let nconstr = Array.length mip.mind_consnames in
+ if Int.equal nconstr 1 then
+ let (ctx, cty) = constr_types.(0) in
+ let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
+ if is_matching env sigma coq_refl_leibniz1_pattern cty then
+ None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
+ else if is_matching env sigma coq_refl_leibniz2_pattern cty then
+ None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+ else if is_matching env sigma coq_refl_jm_pattern cty then
+ None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
+ else raise NoEquationFound
+ else raise NoEquationFound
+ with UserError _ ->
+ raise NoEquationFound)
+ | _ -> raise NoEquationFound
(* Note: An "equality type" is any type with a single argument-free
constructor: it captures eq, eq_dep, JMeq, eq_true, etc. but also
diff --git a/test-suite/bugs/closed/bug_12806.v b/test-suite/bugs/closed/bug_12806.v
new file mode 100644
index 0000000000..ee221d33a6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12806.v
@@ -0,0 +1,9 @@
+Require Import Ltac2.Ltac2.
+
+Declare Scope my_scope.
+Delimit Scope my_scope with my_scope.
+
+Notation "###" := tt : my_scope.
+
+Ltac2 Notation "bar" c(open_constr(my_scope)) := c.
+Ltac2 Eval bar ###.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 457b8e1acf..4758ecf5bd 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1754,6 +1754,16 @@ let () = add_scope "constr" (fun arg ->
Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act)
)
+let () = add_scope "open_constr" (fun arg ->
+ let delimiters = List.map (function
+ | SexprRec (_, { v = Some s }, []) -> s
+ | _ -> scope_fail "open_constr" arg)
+ arg
+ in
+ let act e = Tac2quote.of_open_constr ~delimiters e in
+ Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act)
+ )
+
let add_expr_scope name entry f =
add_scope name begin function
| [] -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm entry, f)
@@ -1782,7 +1792,6 @@ let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_
let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_matching
let () = add_expr_scope "format" Pcoq.Prim.lstring Tac2quote.of_format
-let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr
let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
(** seq scope, a bit hairy *)
diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml
index d1a72fcfd1..2d65f9ec3e 100644
--- a/user-contrib/Ltac2/tac2quote.ml
+++ b/user-contrib/Ltac2/tac2quote.ml
@@ -102,18 +102,22 @@ let of_anti f = function
let of_ident {loc;v=id} = inj_wit ?loc wit_ident id
+let quote_constr ?delimiters c =
+ let loc = Constrexpr_ops.constr_loc c in
+ Option.cata
+ (List.fold_left (fun c d ->
+ CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c))
+ c)
+ c delimiters
+
let of_constr ?delimiters c =
let loc = Constrexpr_ops.constr_loc c in
- let c = Option.cata
- (List.fold_left (fun c d ->
- CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c))
- c)
- c delimiters
- in
+ let c = quote_constr ?delimiters c in
inj_wit ?loc wit_constr c
-let of_open_constr c =
+let of_open_constr ?delimiters c =
let loc = Constrexpr_ops.constr_loc c in
+ let c = quote_constr ?delimiters c in
inj_wit ?loc wit_open_constr c
let of_bool ?loc b =
diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli
index fcd1339cd7..6e2f548319 100644
--- a/user-contrib/Ltac2/tac2quote.mli
+++ b/user-contrib/Ltac2/tac2quote.mli
@@ -36,7 +36,7 @@ val of_ident : Id.t CAst.t -> raw_tacexpr
val of_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr
-val of_open_constr : Constrexpr.constr_expr -> raw_tacexpr
+val of_open_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr
val of_list : ?loc:Loc.t -> ('a -> raw_tacexpr) -> 'a list -> raw_tacexpr
diff --git a/vernac/record.ml b/vernac/record.ml
index fccc3e4fbd..53f3508806 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -766,11 +766,9 @@ let add_inductive_class env sigma ind =
let k =
let ctx = oneind.mind_arity_ctxt in
let univs = Declareops.inductive_polymorphic_context mind in
- let env = push_context ~strict:false (Univ.AUContext.repr univs) env in
- let env = push_rel_context ctx env in
let inst = Univ.make_abstract_instance univs in
let ty = Inductive.type_of_inductive ((mind, oneind), inst) in
- let r = Inductive.relevance_of_inductive env ind in
+ let r = oneind.mind_relevance in
{ cl_univs = univs;
cl_impl = GlobRef.IndRef ind;
cl_context = ctx;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:18:57 +0000