aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/tacinterp.ml59
-rw-r--r--plugins/ltac/tacinterp.mli18
-rw-r--r--test-suite/success/Scopes.v6
3 files changed, 49 insertions, 34 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 2014f2aff3..37fdd185e9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -577,57 +577,47 @@ let extract_ltac_constr_context ist env sigma =
(** Significantly simpler than [interp_constr], to interpret an
untyped constr, it suffices to adjoin a closure environment. *)
-let interp_uconstr ist env sigma = function
- | (term,None) ->
- { closure = extract_ltac_constr_context ist env sigma; term }
- | (_,Some ce) ->
- let ( {typed ; untyped } as closure) = extract_ltac_constr_context ist env sigma in
+let interp_glob_closure ist env sigma ?(kind=WithoutTypeConstraint) ?(pattern_mode=false) (term,term_expr_opt) =
+ let closure = extract_ltac_constr_context ist env sigma in
+ match term_expr_opt with
+ | None -> { closure ; term }
+ | Some term_expr ->
+ (* If at toplevel (term_expr_opt<>None), the error can be due to
+ an incorrect context at globalization time: we retype with the
+ now known intros/lettac/inversion hypothesis names *)
+ let constr_context =
+ Id.Set.union
+ (Id.Map.domain closure.typed)
+ (Id.Map.domain closure.untyped)
+ in
let ltacvars = {
- Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped));
+ ltac_vars = constr_context;
ltac_bound = Id.Map.domain ist.lfun;
ltac_extra = Genintern.Store.empty;
} in
- { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce }
+ { closure ; term = intern_gen kind ~pattern_mode ~ltacvars env term_expr }
-let interp_gen kind ist pattern_mode flags env sigma (c,ce) =
- let constrvars = extract_ltac_constr_context ist env sigma in
+let interp_uconstr ist env sigma c = interp_glob_closure ist env sigma c
+
+let interp_gen kind ist pattern_mode flags env sigma c =
+ let kind_for_intern = match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
+ let { closure = constrvars ; term } =
+ interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in
let vars = {
Pretyping.ltac_constrs = constrvars.typed;
Pretyping.ltac_uconstrs = constrvars.untyped;
Pretyping.ltac_idents = constrvars.idents;
Pretyping.ltac_genargs = ist.lfun;
} in
- let c = match ce with
- | None -> c
- (* If at toplevel (ce<>None), the error can be due to an incorrect
- context at globalization time: we retype with the now known
- intros/lettac/inversion hypothesis names *)
- | Some c ->
- let constr_context =
- Id.Set.union
- (Id.Map.domain constrvars.typed)
- (Id.Set.union
- (Id.Map.domain constrvars.untyped)
- (Id.Map.domain constrvars.idents))
- in
- let ltacvars = {
- ltac_vars = constr_context;
- ltac_bound = Id.Map.domain ist.lfun;
- ltac_extra = Genintern.Store.empty;
- } in
- let kind_for_intern =
- match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
- intern_gen kind_for_intern ~pattern_mode ~ltacvars env c
- in
(* Jason Gross: To avoid unnecessary modifications to tacinterp, as
suggested by Arnaud Spiwack, we run push_trace immediately. We do
this with the kludge of an empty proofview, and rely on the
invariant that running the tactic returned by push_trace does
not modify sigma. *)
let (_, dummy_proofview) = Proofview.init sigma [] in
- let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist) dummy_proofview in
+ let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
let (evd,c) =
- catch_error trace (understand_ltac flags env sigma vars kind) c
+ catch_error trace (understand_ltac flags env sigma vars kind) term
in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
@@ -675,6 +665,9 @@ let pure_open_constr_flags = {
let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c =
interp_gen expected_type ist false flags env sigma c
+let interp_open_constr_with_classes ?(expected_type=WithoutTypeConstraint) ist env sigma c =
+ interp_gen expected_type ist false (open_constr_use_classes_flags ()) env sigma c
+
let interp_pure_open_constr ist =
interp_gen WithoutTypeConstraint ist false pure_open_constr_flags
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 2ec45312ea..fb50a64346 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -72,11 +72,27 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map
val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map ->
Id.t Loc.located -> Id.t
+val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map ->
+ ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr ->
+ Glob_term.closed_glob_constr
+
+val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map ->
+ glob_constr_and_expr -> Glob_term.closed_glob_constr
+
val interp_constr_gen : Pretyping.typing_constraint -> interp_sign ->
Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr
val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
- glob_constr_and_expr bindings -> Evd.evar_map * constr bindings
+ glob_constr_and_expr bindings -> Evd.evar_map * constr bindings
+
+val interp_open_constr : ?expected_type:Pretyping.typing_constraint ->
+ ?flags:Pretyping.inference_flags ->
+ interp_sign -> Environ.env -> Evd.evar_map ->
+ glob_constr_and_expr -> Evd.evar_map * EConstr.constr
+
+val interp_open_constr_with_classes : ?expected_type:Pretyping.typing_constraint ->
+ interp_sign -> Environ.env -> Evd.evar_map ->
+ glob_constr_and_expr -> Evd.evar_map * EConstr.constr
val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
glob_constr_and_expr with_bindings -> Evd.evar_map * EConstr.constr with_bindings
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index 43e3493c1e..ca37467166 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -20,3 +20,9 @@ Inductive U := A.
Bind Scope u with U.
Notation "'ε'" := A : u.
Definition c := ε : U.
+
+(* Check activation of type scope for tactics such as assert *)
+
+Goal True.
+assert (nat * nat).
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:58:03 +0000