aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/topconstr.ml2
-rw-r--r--parsing/pptactic.ml5
-rw-r--r--plugins/quote/quote.ml4
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml22
-rw-r--r--plugins/subtac/subtac_utils.ml1
-rw-r--r--pretyping/evd.ml1
-rw-r--r--pretyping/evd.mli1
-rw-r--r--pretyping/pattern.ml29
-rw-r--r--pretyping/pattern.mli2
-rw-r--r--pretyping/pretyping.ml39
-rw-r--r--pretyping/pretyping.mli7
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/tacexpr.ml6
-rw-r--r--proofs/tactic_debug.mli4
-rw-r--r--tactics/auto.ml12
-rw-r--r--tactics/auto.mli2
-rw-r--r--tactics/class_tactics.ml42
-rw-r--r--tactics/tacinterp.ml100
-rw-r--r--toplevel/himsg.ml2
19 files changed, 146 insertions, 97 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e594f9a9df..155fd1c026 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -381,7 +381,7 @@ let rec subst_aconstr subst bound raw =
AHole (Evd.InternalHole)
| AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType
| Evd.InternalHole | Evd.TomatchTypeParameter _ | Evd.GoalEvar
- | Evd.ImpossibleCase) -> raw
+ | Evd.ImpossibleCase | Evd.MatchingVar _) -> raw
| ACast (r1,k) ->
match k with
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index fe7038d3a3..ad6e2c61bb 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -1043,7 +1043,7 @@ let rec glob_printers =
(pr_glob_tactic_level,
(fun env -> pr_and_constr_expr (pr_rawconstr_env env)),
(fun env -> pr_and_constr_expr (pr_lrawconstr_env env)),
- (fun c -> pr_lconstr_pattern_env (Global.env()) c),
+ (fun (_,c) -> pr_lconstr_pattern_env (Global.env()) c),
(fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))),
(fun env -> pr_or_var (pr_inductive env)),
pr_ltac_or_var (pr_located pr_ltac_constant),
@@ -1083,7 +1083,8 @@ let _ = Tactic_debug.set_match_pattern_printer
let _ = Tactic_debug.set_match_rule_printer
(fun rl ->
- pr_match_rule false (pr_glob_tactic (Global.env())) pr_constr_pattern rl)
+ pr_match_rule false (pr_glob_tactic (Global.env()))
+ (fun (_,p) -> pr_constr_pattern p) rl)
open Extrawit
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 16cc3a7316..e1a16ce498 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -215,9 +215,9 @@ let compute_rhs bodyi index_of_f =
let i = destRel (array_last args) in
PMeta (Some (coerce_meta_in i))
| App (f,args) ->
- PApp (pattern_of_constr f, Array.map aux args)
+ PApp (pattern_of_constr Evd.empty f, Array.map aux args)
| Cast (c,_,_) -> aux c
- | _ -> pattern_of_constr c
+ | _ -> pattern_of_constr Evd.empty c
in
aux bodyi
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 7d1f2cd62e..f909f9e0a9 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -569,7 +569,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
error_unexpected_type_loc
(loc_of_rawconstr c) env ( !evdref) tj.utj_val v
- let pretype_gen fail_evar resolve_classes evdref env lvar kind c =
+ let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
let c' = match kind with
| OfType exptyp ->
let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
@@ -581,7 +581,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
evdref :=
Typeclasses.resolve_typeclasses ~onlyargs:false
~split:true ~fail:fail_evar env !evdref;
- let c = nf_evar !evdref c' in
+ let c = if expand_evar then nf_evar !evdref c' else c' in
if fail_evar then check_evars env Evd.empty !evdref c;
c
@@ -606,30 +606,30 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
fail on unresolved evars; the unsafe_judgment list allows us to
extend env with some bindings *)
- let ise_pretype_gen fail_evar resolve_classes sigma env lvar kind c =
+ let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c =
let evdref = ref (Evd.create_evar_defs sigma) in
- let c = pretype_gen fail_evar resolve_classes evdref env lvar kind c in
+ let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
!evdref, c
(** Entry points of the high-level type synthesis algorithm *)
let understand_gen kind sigma env c =
- snd (ise_pretype_gen true true sigma env ([],[]) kind c)
+ snd (ise_pretype_gen true true true sigma env ([],[]) kind c)
let understand sigma env ?expected_type:exptyp c =
- snd (ise_pretype_gen true true sigma env ([],[]) (OfType exptyp) c)
+ snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c)
let understand_type sigma env c =
- snd (ise_pretype_gen false true sigma env ([],[]) IsType c)
+ snd (ise_pretype_gen true false true sigma env ([],[]) IsType c)
- let understand_ltac sigma env lvar kind c =
- ise_pretype_gen false true sigma env lvar kind c
+ let understand_ltac expand_evar sigma env lvar kind c =
+ ise_pretype_gen expand_evar false true sigma env lvar kind c
let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
- ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c
+ ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
- pretype_gen fail_evar resolve_classes evdref env ([],[]) kind c
+ pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c
end
module Default : S = SubtacPretyping_F(Coercion.Default)
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 476724ba6d..32a1755ca0 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -189,6 +189,7 @@ let string_of_hole_kind = function
| TomatchTypeParameter _ -> "TomatchTypeParameter"
| GoalEvar -> "GoalEvar"
| ImpossibleCase -> "ImpossibleCase"
+ | MatchingVar _ -> "MatchingVar"
let evars_of_term evc init c =
let rec evrec acc c =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0d9a51ba37..ccba1d2cc1 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -32,6 +32,7 @@ type hole_kind =
| TomatchTypeParameter of inductive * int
| GoalEvar
| ImpossibleCase
+ | MatchingVar of bool * identifier
(* The type of mappings for existential variables *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 3974e65b42..b82e6d998d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -94,6 +94,7 @@ type hole_kind =
| TomatchTypeParameter of inductive * int
| GoalEvar
| ImpossibleCase
+ | MatchingVar of bool * identifier
(*********************************************************************)
(*** Existential variables and unification states ***)
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 9acdd15855..7b8c623607 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -89,7 +89,10 @@ let head_of_constr_reference c = match kind_of_term c with
| Var id -> VarRef id
| _ -> anomaly "Not a rigid reference"
-let rec pattern_of_constr t =
+open Evd
+
+let pattern_of_constr sigma t =
+ let rec pattern_of_constr t =
match kind_of_term t with
| Rel n -> PRel n
| Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n)))
@@ -100,11 +103,25 @@ let rec pattern_of_constr t =
| LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
| Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b)
| Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
- | App (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a)
+ | App (f,a) ->
+ (match
+ match kind_of_term f with
+ Evar (evk,args) ->
+ (match snd (Evd.evar_source evk sigma) with
+ MatchingVar (true,n) -> Some n
+ | _ -> None)
+ | _ -> None
+ with
+ | Some n -> PSoApp (n,Array.to_list (Array.map pattern_of_constr a))
+ | None -> PApp (pattern_of_constr f,Array.map (pattern_of_constr) a))
| Const sp -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
| Ind sp -> PRef (canonical_gr (IndRef sp))
| Construct sp -> PRef (canonical_gr (ConstructRef sp))
- | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
+ | Evar (evk,ctxt) ->
+ (match snd (Evd.evar_source evk sigma) with
+ | MatchingVar (b,n) -> assert (not b); PMeta (Some n)
+ | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
+ | _ -> PMeta None)
| Case (ci,p,a,br) ->
let cip = ci.ci_pp_info in
let no = Some (ci.ci_npar,cip.ind_nargs) in
@@ -113,6 +130,7 @@ let rec pattern_of_constr t =
Array.map pattern_of_constr br)
| Fix f -> PFix f
| CoFix f -> PCoFix f
+ in pattern_of_constr t
(* To process patterns, we need a translation without typing at all. *)
@@ -144,11 +162,12 @@ let rec liftn_pattern k n = function
let lift_pattern k = liftn_pattern k 1
-let rec subst_pattern subst pat = match pat with
+let rec subst_pattern subst pat =
+ match pat with
| PRef ref ->
let ref',t = subst_global subst ref in
if ref' == ref then pat else
- pattern_of_constr t
+ pattern_of_constr Evd.empty t
| PVar _
| PEvar _
| PRel _ -> pat
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index b0229ab618..0e87025fc8 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -66,7 +66,7 @@ val head_of_constr_reference : Term.constr -> global_reference
a pattern; currently, no destructor (Cases, Fix, Cofix) and no
existential variable are allowed in [c] *)
-val pattern_of_constr : constr -> constr_pattern
+val pattern_of_constr : Evd.evar_map -> constr -> constr_pattern
(* [pattern_of_rawconstr l c] translates a term [c] with metavariables into
a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 288eb9da22..cfe028aa51 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -108,15 +108,16 @@ sig
(* Generic call to the interpreter from rawconstr to constr, failing
unresolved holes in the rawterm cannot be instantiated.
- In [understand_ltac sigma env ltac_env constraint c],
+ In [understand_ltac expand_evars sigma env ltac_env constraint c],
+ expand_evars : expand inferred evars by their value if any
sigma : initial set of existential variables (typically dependent subgoals)
ltac_env : partial substitution of variables (used for the tactic language)
constraint : tell if interpreted as a possibly constrained term or a type
*)
val understand_ltac :
- evar_map -> env -> var_map * unbound_ltac_var_map ->
+ bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
typing_constraint -> rawconstr -> evar_map * constr
(* Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -156,7 +157,7 @@ sig
rawconstr -> unsafe_type_judgment
val pretype_gen :
- bool -> bool -> evar_map ref -> env ->
+ bool -> bool -> bool -> evar_map ref -> env ->
var_map * (identifier * identifier option) list ->
typing_constraint -> rawconstr -> constr
@@ -307,7 +308,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env evdref j tycon
| RPatVar (loc,(someta,n)) ->
- anomaly "Found a pattern variable in a rawterm to type"
+ let ty =
+ match tycon with
+ | Some (None, ty) -> ty
+ | None | Some _ ->
+ e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+ let k = MatchingVar (someta,n) in
+ { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
| RHole (loc,k) ->
let ty =
@@ -418,7 +425,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let sigma = !evdref in
let c = mkApp (f,Array.map (whd_evar sigma) args) in
let t = Retyping.get_type_of env sigma c in
- make_judge c t
+ make_judge c (* use this for keeping evars: resj.uj_val *) t
| _ -> resj end
| _ -> resj in
inh_conv_coerce_to_tycon loc env evdref resj tycon
@@ -661,7 +668,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
error_unexpected_type_loc
(loc_of_rawconstr c) env !evdref tj.utj_val v
- let pretype_gen fail_evar resolve_classes evdref env lvar kind c =
+ let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
let c' = match kind with
| OfType exptyp ->
let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
@@ -673,7 +680,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
evdref :=
Typeclasses.resolve_typeclasses ~onlyargs:false
~split:true ~fail:fail_evar env !evdref;
- let c = nf_evar !evdref c' in
+ let c = if expand_evar then nf_evar !evdref c' else c' in
if fail_evar then check_evars env Evd.empty !evdref c;
c
@@ -701,30 +708,30 @@ module Pretyping_F (Coercion : Coercion.S) = struct
fail on unresolved evars; the unsafe_judgment list allows us to
extend env with some bindings *)
- let ise_pretype_gen fail_evar resolve_classes sigma env lvar kind c =
+ let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c =
let evdref = ref (Evd.create_evar_defs sigma) in
- let c = pretype_gen fail_evar resolve_classes evdref env lvar kind c in
+ let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
!evdref, c
(** Entry points of the high-level type synthesis algorithm *)
let understand_gen kind sigma env c =
- snd (ise_pretype_gen true true sigma env ([],[]) kind c)
+ snd (ise_pretype_gen true true true sigma env ([],[]) kind c)
let understand sigma env ?expected_type:exptyp c =
- snd (ise_pretype_gen true true sigma env ([],[]) (OfType exptyp) c)
+ snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c)
let understand_type sigma env c =
- snd (ise_pretype_gen true true sigma env ([],[]) IsType c)
+ snd (ise_pretype_gen true true true sigma env ([],[]) IsType c)
- let understand_ltac sigma env lvar kind c =
- ise_pretype_gen false false sigma env lvar kind c
+ let understand_ltac expand_evar sigma env lvar kind c =
+ ise_pretype_gen expand_evar false false sigma env lvar kind c
let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
- ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c
+ ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
- pretype_gen fail_evar resolve_classes evdref env ([],[]) kind c
+ pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c
end
module Default : S = Pretyping_F(Coercion.Default)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index e3b18f73cb..75bd7874e7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -51,15 +51,16 @@ sig
(* Generic call to the interpreter from rawconstr to constr, failing
unresolved holes in the rawterm cannot be instantiated.
- In [understand_ltac sigma env ltac_env constraint c],
+ In [understand_ltac expand_evars sigma env ltac_env constraint c],
+ expand_evars : expand inferred evars by their value if any
sigma : initial set of existential variables (typically dependent subgoals)
ltac_env : partial substitution of variables (used for the tactic language)
constraint : tell if interpreted as a possibly constrained term or a type
*)
val understand_ltac :
- evar_map -> env -> var_map * unbound_ltac_var_map ->
+ bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
typing_constraint -> rawconstr -> evar_map * constr
(* Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -97,7 +98,7 @@ sig
rawconstr -> unsafe_type_judgment
val pretype_gen :
- bool -> bool -> evar_map ref -> env ->
+ bool -> bool -> bool -> evar_map ref -> env ->
var_map * (identifier * identifier option) list ->
typing_constraint -> rawconstr -> constr
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index b3976704af..e4fab3f2f8 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -43,7 +43,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
error "Instantiate called on already-defined evar";
let env = Evd.evar_env evi in
let sigma',typed_c =
- try Pretyping.Default.understand_ltac sigma env ltac_var
+ try Pretyping.Default.understand_ltac true sigma env ltac_var
(Pretyping.OfType (Some evi.evar_concl)) rawc
with _ ->
let loc = Rawterm.loc_of_rawconstr rawc in
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 1d4766494d..04b7a225c7 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -273,7 +273,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg =
(* Globalized tactics *)
and glob_tactic_expr =
(rawconstr_and_expr,
- constr_pattern,
+ rawconstr_and_expr * constr_pattern,
evaluable_global_reference and_short_name or_var,
inductive or_var,
ltac_constant located or_var,
@@ -317,7 +317,7 @@ type raw_red_expr = (constr_expr, reference or_by_notation) red_expr_gen
type glob_atomic_tactic_expr =
(rawconstr_and_expr,
- constr_pattern,
+ rawconstr_and_expr * constr_pattern,
evaluable_global_reference and_short_name or_var,
inductive or_var,
ltac_constant located or_var,
@@ -327,7 +327,7 @@ type glob_atomic_tactic_expr =
type glob_tactic_arg =
(rawconstr_and_expr,
- constr_pattern,
+ rawconstr_and_expr * constr_pattern,
evaluable_global_reference and_short_name or_var,
inductive or_var,
ltac_constant located or_var,
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index ab59f208af..0a5e6087b1 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -24,7 +24,7 @@ val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit
val set_match_pattern_printer :
(env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit
val set_match_rule_printer :
- ((constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
+ ((Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
unit
(* Debug information *)
@@ -41,7 +41,7 @@ val db_constr : debug_info -> env -> constr -> unit
(* Prints the pattern rule *)
val db_pattern_rule :
- debug_info -> int -> (constr_pattern,glob_tactic_expr) match_rule -> unit
+ debug_info -> int -> (Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
(* Prints a matched hypothesis *)
val db_matched_hyp :
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 59791f011d..0e4091b3cb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -268,12 +268,12 @@ let dummy_goal =
{it = make_evar empty_named_context_val mkProp;
sigma = empty}
-let make_exact_entry pri (c,cty) =
+let make_exact_entry sigma pri (c,cty) =
let cty = strip_outer_cast cty in
match kind_of_term cty with
| Prod _ -> failwith "make_exact_entry"
| _ ->
- let pat = Pattern.pattern_of_constr cty in
+ let pat = Pattern.pattern_of_constr sigma cty in
let head =
try head_of_constr_reference (fst (head_constr cty))
with _ -> failwith "make_exact_entry"
@@ -287,7 +287,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
| Prod _ ->
let ce = mk_clenv_from dummy_goal (c,cty) in
let c' = clenv_type (* ~reduce:false *) ce in
- let pat = Pattern.pattern_of_constr c' in
+ let pat = Pattern.pattern_of_constr sigma c' in
let hd = (try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry") in
let nmiss = List.length (clenv_missing ce) in
@@ -317,7 +317,7 @@ let make_resolves env sigma flags pri c =
let ents =
map_succeed
(fun f -> f (c,cty))
- [make_exact_entry pri; make_apply_entry env sigma flags pri]
+ [make_exact_entry sigma pri; make_apply_entry env sigma flags pri]
in
if ents = [] then
errorlabstrm "Hint"
@@ -354,7 +354,7 @@ let make_trivial env sigma c =
let hd = head_of_constr_reference (fst (head_constr t)) in
let ce = mk_clenv_from dummy_goal (c,t) in
(Some hd, { pri=1;
- pat = Some (Pattern.pattern_of_constr (clenv_type ce));
+ pat = Some (Pattern.pattern_of_constr sigma (clenv_type ce));
code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
open Vernacexpr
@@ -1102,7 +1102,7 @@ let make_resolve_any_hyp env sigma (id,_,ty) =
let ents =
map_succeed
(fun f -> f (mkVar id,ty))
- [make_exact_entry None; make_apply_entry env sigma (true,true,false) None]
+ [make_exact_entry sigma None; make_apply_entry env sigma (true,true,false) None]
in
ents
diff --git a/tactics/auto.mli b/tactics/auto.mli
index fe59dc1e12..072e02989a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -112,7 +112,7 @@ val print_hint_db : Hint_db.t -> unit
[c] is the term given as an exact proof to solve the goal;
[ctyp] is the type of [c]. *)
-val make_exact_entry : int option -> constr * constr -> hint_entry
+val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry
(* [make_apply_entry (eapply,verbose) pri (c,cty)].
[eapply] is true if this hint will be used only with EApply;
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6f928e0966..b77425f0d6 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -271,7 +271,7 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
if keep then let c = mkVar id in
map_succeed
(fun f -> try f (c,cty) with UserError _ -> failwith "")
- [make_exact_entry pri; make_apply_entry env sigma flags pri]
+ [make_exact_entry sigma pri; make_apply_entry env sigma flags pri]
else []
let pf_filtered_hyps gls =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bef5563454..f031df2560 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -497,15 +497,15 @@ let intern_binding_name ist x =
and if a term w/o ltac vars, check the name is indeed quantified *)
x
-let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
+let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
let c' =
- warn (Constrintern.intern_gen isarity ~ltacvars:(fst lfun,[]) sigma env) c
+ warn (Constrintern.intern_gen isarity ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c
in
(c',if !strict_check then None else Some c)
-let intern_constr = intern_constr_gen false
-let intern_type = intern_constr_gen true
+let intern_constr = intern_constr_gen false false
+let intern_type = intern_constr_gen false true
(* Globalize bindings *)
let intern_binding ist (loc,b,c) =
@@ -604,15 +604,17 @@ let intern_hyp_location ist (((b,occs),id),hl) =
(((b,List.map (intern_or_var ist) occs),intern_hyp_or_metaid ist id), hl)
(* Reads a pattern *)
-let intern_pattern sigma env ?(as_type=false) lfun = function
+let intern_pattern ist ?(as_type=false) lfun = function
| Subterm (b,ido,pc) ->
let ltacvars = (lfun,[]) in
- let (metas,pat) = intern_constr_pattern sigma env ~ltacvars pc in
- ido, metas, Subterm (b,ido,pat)
+ let (metas,pat) = intern_constr_pattern ist.gsigma ist.genv ~ltacvars pc in
+ let c = intern_constr_gen true false ist pc in
+ ido, metas, Subterm (b,ido,(c,pat))
| Term pc ->
let ltacvars = (lfun,[]) in
- let (metas,pat) = intern_constr_pattern sigma env ~as_type ~ltacvars pc in
- None, metas, Term pat
+ let (metas,pat) = intern_constr_pattern ist.gsigma ist.genv ~as_type ~ltacvars pc in
+ let c = intern_constr_gen true false ist pc in
+ None, metas, Term (c,pat)
let intern_constr_may_eval ist = function
| ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c)
@@ -649,16 +651,16 @@ let extend_values_with_bindings (ln,lm) lfun =
lmatch@lfun@lnames
(* Reads the hypotheses of a "match goal" rule *)
-let rec intern_match_goal_hyps sigma env lfun = function
+let rec intern_match_goal_hyps ist lfun = function
| (Hyp ((_,na) as locna,mp))::tl ->
- let ido, metas1, pat = intern_pattern sigma env ~as_type:true lfun mp in
- let lfun, metas2, hyps = intern_match_goal_hyps sigma env lfun tl in
+ let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
+ let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
let lfun' = name_cons na (Option.List.cons ido lfun) in
lfun', metas1@metas2, Hyp (locna,pat)::hyps
| (Def ((_,na) as locna,mv,mp))::tl ->
- let ido, metas1, patv = intern_pattern sigma env ~as_type:false lfun mv in
- let ido', metas2, patt = intern_pattern sigma env ~as_type:true lfun mp in
- let lfun, metas3, hyps = intern_match_goal_hyps sigma env lfun tl in
+ let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
+ let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
+ let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in
let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in
lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
| [] -> lfun, [], []
@@ -714,7 +716,7 @@ let rec intern_atomic lf ist x =
| TacAssert (otac,ipat,c) ->
TacAssert (Option.map (intern_tactic ist) otac,
Option.map (intern_intro_pattern lf ist) ipat,
- intern_constr_gen (otac<>None) ist c)
+ intern_constr_gen false (otac<>None) ist c)
| TacGeneralize cl ->
TacGeneralize (List.map (fun (c,na) ->
intern_constr_with_occurrences ist c,
@@ -904,8 +906,8 @@ and intern_match_rule ist = function
All (intern_tactic ist tc) :: (intern_match_rule ist tl)
| (Pat (rl,mp,tc))::tl ->
let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
- let lfun',metas1,hyps = intern_match_goal_hyps sigma env lfun rl in
- let ido,metas2,pat = intern_pattern sigma env lfun mp in
+ let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
+ let ido,metas2,pat = intern_pattern ist lfun mp in
let metas = list_uniquize (metas1@metas2) in
let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl)
@@ -1312,7 +1314,7 @@ let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
(* Side-effect *)
!evdref,c
-let interp_gen kind ist fail_evar use_classes env sigma (c,ce) =
+let interp_gen kind ist expand_evar fail_evar use_classes env sigma (c,ce) =
let (ltacvars,unbndltacvars as vars),typs =
extract_ltac_vars_data ist sigma env in
let c = match ce with
@@ -1325,25 +1327,34 @@ let interp_gen kind ist fail_evar use_classes env sigma (c,ce) =
intern_gen (kind = IsType) ~ltacvars:ltacdata sigma env c in
let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
let evd,c =
- catch_error trace (understand_ltac sigma env (typs,unbndltacvars) kind) c in
- let evd,c = solve_remaining_evars fail_evar use_classes env sigma evd c in
+ catch_error trace
+ (understand_ltac expand_evar sigma env (typs,unbndltacvars) kind) c in
+ let evd,c =
+ if expand_evar then
+ solve_remaining_evars fail_evar use_classes env sigma evd c
+ else
+ evd,c in
db_constr ist.debug env c;
(evd,c)
(* Interprets a constr; expects evars to be solved *)
let interp_constr_gen kind ist env sigma c =
- snd (interp_gen kind ist true true env sigma c)
+ snd (interp_gen kind ist true true true env sigma c)
let interp_constr = interp_constr_gen (OfType None)
let interp_type = interp_constr_gen IsType
(* Interprets an open constr *)
-let interp_open_constr_gen kind ist = interp_gen kind ist false false
+let interp_open_constr_gen kind ist = interp_gen kind ist true false false
let interp_open_constr ccl =
interp_open_constr_gen (OfType ccl)
+let interp_typed_pattern ist env sigma c =
+ let sigma, c = interp_gen (OfType None) ist false false false env sigma c in
+ pattern_of_constr sigma c
+
(* Interprets a constr expression casted by the current goal *)
let pf_interp_casted_constr ist gl c =
interp_constr_gen (OfType (Some (pf_concl gl))) ist (pf_env gl) (project gl) c
@@ -1626,13 +1637,18 @@ let give_context ctxt = function
| Some id -> [id,VConstr_context ctxt]
(* Reads a pattern by substituting vars of lfun *)
-let eval_pattern lfun c =
- let lvar = List.map (fun (id,c) -> (id,lazy(pattern_of_constr c))) lfun in
- instantiate_pattern lvar c
+let use_types = false
+
+let eval_pattern lfun ist env sigma (c,pat) =
+ if use_types then
+ interp_typed_pattern ist env sigma c
+ else
+ let lvar = List.map (fun (id,c) -> (id,lazy(pattern_of_constr Evd.empty c))) lfun in
+ instantiate_pattern lvar pat
-let read_pattern lfun = function
- | Subterm (b,ido,pc) -> Subterm (b,ido,eval_pattern lfun pc)
- | Term pc -> Term (eval_pattern lfun pc)
+let read_pattern lfun ist env sigma = function
+ | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
+ | Term c -> Term (eval_pattern lfun ist env sigma c)
(* Reads the hypotheses of a Match Context rule *)
let cons_and_check_name id l =
@@ -1642,23 +1658,23 @@ let cons_and_check_name id l =
" used twice in the same pattern."))
else id::l
-let rec read_match_goal_hyps lfun lidh = function
+let rec read_match_goal_hyps lfun ist env sigma lidh = function
| (Hyp ((loc,na) as locna,mp))::tl ->
let lidh' = name_fold cons_and_check_name na lidh in
- Hyp (locna,read_pattern lfun mp)::
- (read_match_goal_hyps lfun lidh' tl)
+ Hyp (locna,read_pattern lfun ist env sigma mp)::
+ (read_match_goal_hyps lfun ist env sigma lidh' tl)
| (Def ((loc,na) as locna,mv,mp))::tl ->
let lidh' = name_fold cons_and_check_name na lidh in
- Def (locna,read_pattern lfun mv, read_pattern lfun mp)::
- (read_match_goal_hyps lfun lidh' tl)
+ Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp)::
+ (read_match_goal_hyps lfun ist env sigma lidh' tl)
| [] -> []
(* Reads the rules of a Match Context or a Match *)
-let rec read_match_rule lfun = function
- | (All tc)::tl -> (All tc)::(read_match_rule lfun tl)
+let rec read_match_rule lfun ist env sigma = function
+ | (All tc)::tl -> (All tc)::(read_match_rule lfun ist env sigma tl)
| (Pat (rl,mp,tc))::tl ->
- Pat (read_match_goal_hyps lfun [] rl, read_pattern lfun mp,tc)
- :: read_match_rule lfun tl
+ Pat (read_match_goal_hyps lfun ist env sigma [] rl, read_pattern lfun ist env sigma mp,tc)
+ :: read_match_rule lfun ist env sigma tl
| [] -> []
(* For Match Context and Match *)
@@ -1989,7 +2005,7 @@ and interp_match_goal ist goal lz lr lmr =
else mt()) ++ str"."))
end in
apply_match_goal ist env goal 0 lmr
- (read_match_rule (fst (constr_list ist env)) lmr)
+ (read_match_rule (fst (constr_list ist env)) ist env (project goal) lmr)
(* Tries to match the hypotheses in a Match Context *)
and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
@@ -2158,7 +2174,7 @@ and interp_match ist g lz constr lmr =
debugging_exception_step ist true e
(fun () -> str "evaluation of the matched expression");
raise e in
- let ilr = read_match_rule (fst (constr_list ist (pf_env g))) lmr in
+ let ilr = read_match_rule (fst (constr_list ist (pf_env g))) ist (pf_env g) (project g) lmr in
let res =
try apply_match ist csr ilr with e ->
debugging_exception_step ist true e (fun () -> str "match expression");
@@ -2589,8 +2605,8 @@ let subst_raw_may_eval subst = function
| ConstrTerm c -> ConstrTerm (subst_rawconstr subst c)
let subst_match_pattern subst = function
- | Subterm (b,ido,pc) -> Subterm (b,ido,subst_pattern subst pc)
- | Term pc -> Term (subst_pattern subst pc)
+ | Subterm (b,ido,(c,pc)) -> Subterm (b,ido,(subst_rawconstr subst c,subst_pattern subst pc))
+ | Term (c,pc) -> Term (subst_rawconstr subst c,subst_pattern subst pc)
let rec subst_match_goal_hyps subst = function
| Hyp (locs,mp) :: tl ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 852e7588af..fdd05b870f 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -350,6 +350,8 @@ let explain_hole_kind env evi = function
str "an existential variable"
| ImpossibleCase ->
str "the type of an impossible pattern-matching clause"
+ | MatchingVar _ ->
+ assert false
let explain_not_clean env ev t k =
let env = make_all_name_different env in
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-22 14:42:46 +0000