aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES3
-rw-r--r--Makefile14
-rw-r--r--contrib/first-order/instances.ml4
-rw-r--r--contrib/recdef/recdef.ml428
-rw-r--r--pretyping/clenv.ml211
-rw-r--r--pretyping/clenv.mli12
-rw-r--r--pretyping/evd.ml25
-rw-r--r--pretyping/evd.mli8
-rw-r--r--pretyping/reductionops.ml28
-rw-r--r--pretyping/reductionops.mli1
-rw-r--r--pretyping/termops.ml10
-rw-r--r--pretyping/termops.mli2
-rw-r--r--pretyping/unification.ml80
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/equality.ml31
-rw-r--r--tactics/equality.mli4
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/hiddentac.ml8
-rw-r--r--tactics/inv.ml13
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/setoid_replace.ml2
-rw-r--r--tactics/tacticals.ml4
-rw-r--r--tactics/tactics.ml81
-rw-r--r--tactics/tactics.mli21
-rw-r--r--test-suite/success/apply.v65
25 files changed, 421 insertions, 240 deletions
diff --git a/CHANGES b/CHANGES
index ea73490d7..b1d42a03a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,6 +45,9 @@ Tactics
- Better heuristic of lemma unfolding for apply/eapply.
- New tactics "eapply in", "erewrite", "erewrite in".
- Unfoldable references can be given by notation rather than by name in unfold.
+- The "with" arguments are now typed using informations from the current goal:
+ allows support for coercions and more inference of implicit arguments.
+- Application of "f_equal"-style lemmas works better.
Miscellaneous
diff --git a/Makefile b/Makefile
index 2de542be2..88beb3d50 100644
--- a/Makefile
+++ b/Makefile
@@ -155,9 +155,9 @@ PRETYPING=\
pretyping/reductionops.cmo pretyping/vnorm.cmo pretyping/inductiveops.cmo \
pretyping/retyping.cmo pretyping/cbv.cmo \
pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \
- pretyping/tacred.cmo \
- pretyping/evarutil.cmo pretyping/unification.cmo pretyping/evarconv.cmo \
- pretyping/classops.cmo pretyping/coercion.cmo pretyping/clenv.cmo \
+ pretyping/tacred.cmo pretyping/evarutil.cmo pretyping/evarconv.cmo \
+ pretyping/classops.cmo pretyping/coercion.cmo \
+ pretyping/unification.cmo pretyping/clenv.cmo \
pretyping/rawterm.cmo pretyping/pattern.cmo \
pretyping/detyping.cmo pretyping/indrec.cmo\
pretyping/cases.cmo pretyping/pretyping.cmo pretyping/matching.cmo
@@ -1497,14 +1497,14 @@ PRINTERSCMO=\
library/summary.cmo library/global.cmo library/nameops.cmo \
library/libnames.cmo library/nametab.cmo library/libobject.cmo \
library/lib.cmo library/goptions.cmo \
- pretyping/termops.cmo pretyping/evd.cmo \
- pretyping/rawterm.cmo pretyping/termops.cmo pretyping/evd.cmo \
+ pretyping/termops.cmo pretyping/evd.cmo pretyping/rawterm.cmo \
pretyping/reductionops.cmo pretyping/inductiveops.cmo \
pretyping/retyping.cmo pretyping/cbv.cmo \
pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \
- pretyping/evarutil.cmo pretyping/unification.cmo pretyping/evarconv.cmo \
+ pretyping/evarutil.cmo pretyping/evarconv.cmo \
pretyping/tacred.cmo pretyping/classops.cmo pretyping/detyping.cmo \
- pretyping/indrec.cmo pretyping/coercion.cmo pretyping/cases.cmo \
+ pretyping/indrec.cmo pretyping/coercion.cmo \
+ pretyping/unification.cmo pretyping/cases.cmo \
pretyping/pretyping.cmo pretyping/clenv.cmo pretyping/pattern.cmo \
parsing/lexer.cmo interp/ppextend.cmo interp/genarg.cmo \
interp/topconstr.cmo interp/notation.cmo interp/reserve.cmo \
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index fac39df93..8eeb8b642 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -182,11 +182,11 @@ let right_instance_tac inst continue seq=
[introf;
(fun gls->
split (Rawterm.ImplicitBindings
- [inj_open (mkVar (Tacmach.pf_nth_hyp_id gls 1))]) gls);
+ [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
tclSOLVE [wrap 0 true continue (deepen seq)]];
tclTRY assumption]
| Real ((0,t),_) ->
- (tclTHEN (split (Rawterm.ImplicitBindings [inj_open t]))
+ (tclTHEN (split (Rawterm.ImplicitBindings [t]))
(tclSOLVE [wrap 0 true continue (deepen seq)]))
| Real ((m,t),_) ->
tclFAIL 0 (Pp.str "not implemented ... yet")
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 49791c367..5f45d9d85 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -8,6 +8,8 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
+(* $Id:$ *)
+
open Term
open Termops
open Environ
@@ -416,8 +418,8 @@ let base_leaf_terminate (func:global_reference) eqs expr =
[k';h] -> k',h
| _ -> assert false
in
- tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [inj_open expr]));
- observe_tac "second split" (split (ImplicitBindings [inj_open (delayed_force coq_O)]));
+ tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [expr]));
+ observe_tac "second split" (split (ImplicitBindings [delayed_force coq_O]));
observe_tac "intro k" (h_intro k');
observe_tac "case on k"
(tclTHENS
@@ -459,7 +461,7 @@ let rec compute_le_proofs = function
in
apply_with_bindings
(le_trans,
- ExplicitBindings[dummy_loc,NamedHyp m_id,inj_open a])
+ ExplicitBindings[dummy_loc,NamedHyp m_id,a])
g
)
[compute_le_proofs tl;
@@ -477,7 +479,7 @@ let make_lt_proof pmax le_proof =
in
apply_with_bindings
(le_lt_trans,
- ExplicitBindings[dummy_loc,NamedHyp m_id, inj_open pmax]) g)
+ ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g)
[observe_tac "compute_le_proofs" (compute_le_proofs le_proof);
tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];;
@@ -496,8 +498,8 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
tclTHENS
(general_rewrite_bindings false
(mkVar eq,
- ExplicitBindings[dummy_loc, NamedHyp k_id, inj_open (mkVar k);
- dummy_loc, NamedHyp def_id, inj_open (mkVar def)]) false)
+ ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
+ dummy_loc, NamedHyp def_id, mkVar def]) false)
[list_cond_rewrite k def pmax eqs le_proofs;
observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g
)
@@ -515,7 +517,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
let ids = h'::ids in
let def = next_global_ident_away true def_id ids in
tclTHENLIST
- [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [inj_open s_max]));
+ [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max]));
observe_tac "introduce_all_equalities_final intro k" (h_intro k);
tclTHENS
(observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k)))
@@ -575,8 +577,8 @@ let rec introduce_all_values is_mes acc_inv func context_fn
(match args with
[] ->
tclTHENLIST
- [observe_tac "split" (split(ImplicitBindings
- [inj_open (context_fn (List.map mkVar (List.rev values)))]));
+ [observe_tac "split" (split(ImplicitBindings
+ [context_fn (List.map mkVar (List.rev values))]));
observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs
(List.rev values) (List.rev specs) (delayed_force coq_O) [] [])]
| arg::args ->
@@ -1194,9 +1196,9 @@ let rec introduce_all_values_eq cont_tac functional termine
general_rewrite_bindings false
(mkVar heq1,
ExplicitBindings[dummy_loc,NamedHyp k_id,
- inj_open (f_S(f_S(mkVar pmax)));
+ f_S(f_S(mkVar pmax));
dummy_loc,NamedHyp def_id,
- inj_open f]) false gls )
+ f]) false gls )
[tclTHENLIST
[simpl_iter();
unfold_constr (reference_of_constr functional);
@@ -1247,8 +1249,8 @@ let rec introduce_all_values_eq cont_tac functional termine
(mkVar heq,
ExplicitBindings
[dummy_loc, NamedHyp k_id,
- inj_open (f_S(mkVar pmax'));
- dummy_loc, NamedHyp def_id, inj_open f]) false))
+ f_S(mkVar pmax');
+ dummy_loc, NamedHyp def_id, f]) false))
g
)
[tclIDTAC;
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index c563688a8..96facdef2 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -30,10 +30,13 @@ open Coercion.Default
(* *)
let w_coerce env c ctyp target evd =
- let j = make_judge c ctyp in
- let tycon = mk_tycon_type target in
- let (evd',j') = inh_conv_coerce_to dummy_loc env evd j tycon in
- (evd',j'.uj_val)
+ try
+ let j = make_judge c ctyp in
+ let tycon = mk_tycon_type target in
+ let (evd',j') = inh_conv_coerce_to dummy_loc env evd j tycon in
+ (evd',j'.uj_val)
+ with e when precatchable_exception e ->
+ evd,c
let pf_env gls = Global.env_of_context gls.it.evar_hyps
let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c
@@ -209,17 +212,6 @@ let clenv_wtactic f clenv = {clenv with evd = f clenv.evd }
* type of clenv.
* If [hyps_only] then metavariables occurring in the type are _excluded_ *)
-(* collects all metavar occurences, in left-to-right order, preserving
- * repetitions and all. *)
-
-let collect_metas c =
- let rec collrec acc c =
- match kind_of_term c with
- | Meta mv -> mv::acc
- | _ -> fold_constr collrec acc c
- in
- List.rev (collrec [] c)
-
(* [clenv_metavars clenv mv]
* returns a list of the metavars which appear in the type of
* the metavar mv. The list is unordered. *)
@@ -248,12 +240,34 @@ let clenv_missing ce = clenv_dependent true ce
let clenv_unify allow_K cv_pb t1 t2 clenv =
{ clenv with evd = w_unify allow_K clenv.env cv_pb t1 t2 clenv.evd }
+let clenv_unify_meta_types clenv =
+ List.fold_left (fun clenv (k,m) ->
+ match m with
+ | Cltyp _ -> clenv
+ | Clval (na,(c,s),k_typ) ->
+ let k_typ = clenv_hnf_constr clenv k_typ.rebus in
+ match s with
+ | Coercible c_typ when not (occur_meta k_typ) ->
+ let evd,c' = w_coerce (cl_env clenv) c.rebus c_typ k_typ clenv.evd in
+ {clenv with evd = meta_reassign k (c',ConvUpToEta 0) clenv.evd}
+ | _ ->
+ (* nf_betaiota was before in type_of - useful to reduce
+ types like (x:A)([x]P u) *)
+ let c_typ = nf_betaiota (clenv_get_type_of clenv c.rebus) in
+ let c_typ = clenv_hnf_constr clenv c_typ in
+ (* Try to infer some Meta/Evar from the type of [c] *)
+ try clenv_unify true CUMUL c_typ k_typ clenv
+ with e when precatchable_exception e -> clenv)
+ clenv (meta_list clenv.evd)
+
+
let clenv_unique_resolver allow_K clenv gl =
if isMeta (fst (whd_stack clenv.templtyp.rebus)) then
- clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv
+ clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl)
+ (clenv_unify_meta_types clenv)
else
- try clenv_unify allow_K CUMUL clenv.templtyp.rebus (pf_concl gl) clenv
- with _ -> clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv
+ clenv_unify allow_K CUMUL
+ (meta_reducible_instance clenv.evd clenv.templtyp) (pf_concl gl) clenv
(* [clenv_pose_dependent_evars clenv]
* For each dependent evar in the clause-env which does not have a value,
@@ -326,7 +340,7 @@ let clenv_fchain mv clenv nextclenv =
(***************************************************************)
(* Bindings *)
-type arg_bindings = (int * open_constr) list
+type arg_bindings = open_constr explicit_bindings
(* [clenv_independent clenv]
* returns a list of metavariables which appear in the term cval,
@@ -340,22 +354,24 @@ let clenv_independent clenv =
let deps = dependent_metas clenv mvs ctyp_mvs in
List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
-let meta_of_binder clause loc b t mvs =
- match b with
- | NamedHyp s ->
- if List.exists (fun (_,b',_) -> b=b') t then
- errorlabstrm ""
- (str "The variable " ++ pr_id s ++
- str " occurs more than once in binding");
- meta_with_name clause.evd s
- | AnonHyp n ->
- if List.exists (fun (_,b',_) -> b=b') t then
- errorlabstrm ""
- (str "The position " ++ int n ++
- str " occurs more than once in binding");
- try List.nth mvs (n-1)
- with (Failure _|Invalid_argument _) ->
- errorlabstrm "" (str "No such binder")
+let check_bindings bl =
+ match list_duplicates (List.map pi2 bl) with
+ | NamedHyp s :: _ ->
+ errorlabstrm ""
+ (str "The variable " ++ pr_id s ++
+ str " occurs more than once in binding list");
+ | AnonHyp n :: _ ->
+ errorlabstrm ""
+ (str "The position " ++ int n ++
+ str " occurs more than once in binding list")
+ | [] -> ()
+
+let meta_of_binder clause loc mvs = function
+ | NamedHyp s -> meta_with_name clause.evd s
+ | AnonHyp n ->
+ try List.nth mvs (n-1)
+ with (Failure _|Invalid_argument _) ->
+ errorlabstrm "" (str "No such binder")
let error_already_defined b =
match b with
@@ -367,92 +383,49 @@ let error_already_defined b =
anomalylabstrm ""
(str "Position " ++ int n ++ str" already defined")
-let clenv_match_args s clause =
- let mvs = clenv_independent clause in
- let rec matchrec clenv = function
- | [] -> clenv
- | (loc,b,(sigma,c))::t ->
- let k = meta_of_binder clenv loc b t mvs in
+let clenv_match_args bl clenv =
+ if bl = [] then
+ clenv
+ else
+ let mvs = clenv_independent clenv in
+ check_bindings bl;
+ List.fold_left
+ (fun clenv (loc,b,(sigma,c)) ->
+ let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
- if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then
- matchrec clenv t
+ if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
else error_already_defined b
else
- let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
- (* nf_betaiota was before in type_of - useful to reduce
- types like (x:A)([x]P u) *)
- let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
- let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in
- let c_typ = clenv_hnf_constr clenv' c_typ in
- let clenv'' =
- (* Try to infer some Meta/Evar from the type of [c] *)
- try clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clenv')
- with e when precatchable_exception e ->
- (* Try to coerce to the type of [k]; cannot merge with the
- previous case because Coercion does not handle Meta *)
- let (evd,c') = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in
- try clenv_unify true CONV (mkMeta k) c' { clenv' with evd = evd }
- with PretypeError (env,CannotUnify (m,n)) ->
- Stdpp.raise_with_loc loc
- (PretypeError (env,CannotUnifyBindingType (m,n)))
- in matchrec clenv'' t
- in
- matchrec clause s
-
-
-let clenv_constrain_with_bindings bl clause =
- if bl = [] then
- clause
- else
- let all_mvs = collect_metas clause.templval.rebus in
- let rec matchrec clause = function
- | [] -> clause
- | (n,(sigma,c))::t ->
- let k =
- (try
- if n > 0 then
- List.nth all_mvs (n-1)
- else if n < 0 then
- List.nth (List.rev all_mvs) (-n-1)
- else error "clenv_constrain_with_bindings"
- with Failure _ ->
- errorlabstrm "clenv_constrain_with_bindings"
- (str"Clause did not have " ++ int n ++ str"-th" ++
- str" absolute argument")) in
- let k_typ = nf_betaiota (clenv_meta_type clause k) in
- let cl = { clause with evd = evar_merge clause.evd sigma} in
- let c_typ = nf_betaiota (clenv_get_type_of cl c) in
- matchrec
- (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
- in
- matchrec clause bl
-
-
-(* not exported: maybe useful ? *)
-let clenv_constrain_dep_args hyps_only clause = function
- | [] -> clause
- | mlist ->
- let occlist = clenv_dependent hyps_only clause in
- if List.length occlist = List.length mlist then
- List.fold_left2
- (fun clenv k (sigma,c) ->
- let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
- let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
- let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in
- try
- (* faire quelque chose avec le sigma retourne ? *)
- let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in
- clenv_unify true CONV (mkMeta k) c' { clenv' with evd = evd }
- with _ ->
- clenv_unify true CONV (mkMeta k) c clenv')
- clause occlist mlist
- else
- error ("Not the right number of missing arguments (expected "
- ^(string_of_int (List.length occlist))^")")
-
-let clenv_constrain_missing_args mlist clause =
- clenv_constrain_dep_args true clause mlist
-
+ let c_typ = nf_betaiota (clenv_get_type_of clenv c) in
+ let c_typ = clenv_hnf_constr clenv c_typ in
+ let clenv = { clenv with evd = evar_merge clenv.evd sigma} in
+ {clenv with evd = meta_assign k (c,Coercible c_typ) clenv.evd})
+ clenv bl
+
+let clenv_assign_binding clenv k (sigma,c) =
+ let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
+ let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
+ let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in
+ let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in
+ { clenv' with evd = meta_assign k (c',Coercible c_typ) evd }
+
+let clenv_constrain_last_binding c clenv =
+ let all_mvs = collect_metas clenv.templval.rebus in
+ let k =
+ try list_last all_mvs
+ with Failure _ -> error "clenv_constrain_with_bindings" in
+ clenv_assign_binding clenv k (Evd.empty,c)
+
+let clenv_constrain_dep_args hyps_only bl clenv =
+ if bl = [] then
+ clenv
+ else
+ let occlist = clenv_dependent hyps_only clenv in
+ if List.length occlist = List.length bl then
+ List.fold_left2 clenv_assign_binding clenv occlist bl
+ else
+ error ("Not the right number of missing arguments (expected "
+ ^(string_of_int (List.length occlist))^")")
(****************************************************************)
(* Clausal environment for an application *)
@@ -460,7 +433,7 @@ let clenv_constrain_missing_args mlist clause =
let make_clenv_binding_gen hyps_only n gls (c,t) = function
| ImplicitBindings largs ->
let clause = mk_clenv_from_n gls n (c,t) in
- clenv_constrain_dep_args hyps_only clause largs
+ clenv_constrain_dep_args hyps_only largs clause
| ExplicitBindings lbind ->
let clause = mk_clenv_rename_from_n gls n (c,t) in
clenv_match_args lbind clause
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index b9ee5dde4..ccaa22f5e 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -84,18 +84,20 @@ val clenv_pose_dependent_evars : clausenv -> clausenv
(***************************************************************)
(* Bindings *)
+type arg_bindings = open_constr explicit_bindings
+
(* bindings where the key is the position in the template of the
clenv (dependent or not). Positions can be negative meaning to
start from the rightmost argument of the template. *)
-type arg_bindings = (int * open_constr) list
-
val clenv_independent : clausenv -> metavariable list
val clenv_missing : clausenv -> metavariable list
+val clenv_constrain_last_binding : constr -> clausenv -> clausenv
+
(* defines metas corresponding to the name of the bindings *)
-val clenv_match_args :
- open_constr explicit_bindings -> clausenv -> clausenv
-val clenv_constrain_with_bindings : arg_bindings -> clausenv -> clausenv
+val clenv_match_args : arg_bindings -> clausenv -> clausenv
+
+val clenv_unify_meta_types : clausenv -> clausenv
(* start with a clenv to refine with a given term with bindings *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1ff0c633a..ebd635b80 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -334,7 +334,8 @@ let map_fl f cfl = { cfl with rebus=f cfl.rebus }
(e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
*)
-type instance_status = IsSuperType | IsSubType | ConvUpToEta of int
+type instance_status =
+ IsSuperType | IsSubType | ConvUpToEta of int | Coercible of types
(* Clausal environments *)
@@ -535,6 +536,28 @@ let meta_merge evd1 evd2 =
metas = List.fold_left (fun m (n,v) -> Metamap.add n v m)
evd2.metas (metamap_to_list evd1.metas) }
+type metabinding = metavariable * constr * instance_status
+
+let retract_defined_metas evd =
+ let mc,ml =
+ Metamap.fold (fun n v (mc,ml) ->
+ match v with
+ | Clval (na,(b,s),typ) ->
+ (n,b.rebus,s)::mc, Metamap.add n (Cltyp (na,typ)) ml
+ | Cltyp _ as v ->
+ mc, Metamap.add n v ml)
+ evd.metas ([],Metamap.empty) in
+ mc, { evd with metas = ml }
+
+let rec list_assoc_in_triple x = function
+ [] -> raise Not_found
+ | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_in_triple x l
+
+let subst_defined_metas bl c =
+ let rec substrec c = match kind_of_term c with
+ | Meta i -> list_assoc_in_triple i bl
+ | _ -> map_constr substrec c
+ in try Some (substrec c) with Not_found -> None
(**********************************************************)
(* Pretty-printing *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a1323e501..784e066b7 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -111,7 +111,8 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
(e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
*)
-type instance_status = IsSuperType | IsSubType | ConvUpToEta of int
+type instance_status =
+ IsSuperType | IsSubType | ConvUpToEta of int | Coercible of types
type clbinding =
| Cltyp of name * constr freelisted
@@ -177,6 +178,11 @@ val meta_merge : evar_defs -> evar_defs -> evar_defs
val metas_of : evar_defs -> metamap
+type metabinding = metavariable * constr * instance_status
+
+val retract_defined_metas : evar_defs -> metabinding list * evar_defs
+val subst_defined_metas : metabinding list -> constr -> constr option
+
(**********************************************************)
(* Sort variables *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 481fa16ee..3e9b08beb 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -879,3 +879,31 @@ let meta_instance env b =
instance c_sigma b.rebus
let nf_meta env c = meta_instance env (mk_freelisted c)
+
+(* Instantiate metas that create beta/iota redexes *)
+
+let meta_reducible_instance env b =
+ let s =
+ List.map (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
+ in
+ let rec irec u =
+ let u = whd_betaiota u in
+ match kind_of_term u with
+ | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
+ let bl' = Array.map irec bl in
+ let p' = irec p in
+ let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
+ let g = List.assoc m s in
+ (match kind_of_term g with
+ | Construct _ -> whd_betaiota (mkCase (ci,p',g,bl'))
+ | _ -> mkCase (ci,p',c,bl'))
+ | App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) ->
+ let l' = Array.map irec l in
+ let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in
+ let g = List.assoc m s in
+ (match kind_of_term g with
+ | Lambda _ -> beta_appvect g l'
+ | _ -> mkApp (f,l'))
+ | _ -> map_constr irec u
+ in
+ if s = [] then b.rebus else irec b.rebus
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 8c792dc80..2dbf60a42 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -217,3 +217,4 @@ val apprec : state_reduction_function
(*s Meta-related reduction functions *)
val meta_instance : evar_defs -> constr freelisted -> constr
val nf_meta : evar_defs -> constr -> constr
+val meta_reducible_instance : evar_defs -> constr freelisted -> constr
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 6597ce5a3..668b3a1eb 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -514,6 +514,16 @@ let free_rels m =
in
frec 1 Intset.empty m
+(* collects all metavar occurences, in left-to-right order, preserving
+ * repetitions and all. *)
+
+let collect_metas c =
+ let rec collrec acc c =
+ match kind_of_term c with
+ | Meta mv -> mv::acc
+ | _ -> fold_constr collrec acc c
+ in
+ List.rev (collrec [] c)
(* (dependent M N) is true iff M is eq_term with a subterm of N
M is appropriately lifted through abstractions of N *)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 7fbd130ca..27e86a6ca 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -102,7 +102,7 @@ val occur_var_in_decl :
val occur_term : constr -> constr -> bool
val free_rels : constr -> Intset.t
val dependent : constr -> constr -> bool
-
+val collect_metas : constr -> int list
(* Substitution of metavariables *)
type metamap = (metavariable * constr) list
val subst_meta : metamap -> constr -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5231cce42..e296737f2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -65,7 +65,7 @@ let prod_pb = function ConvUnderApp _ -> topconv | pb -> pb
let opp_status = function
| IsSuperType -> IsSubType
| IsSubType -> IsSuperType
- | ConvUpToEta _ as x -> x
+ | ConvUpToEta _ | Coercible _ as x -> x
let extract_instance_status = function
| Cumul -> (IsSubType,IsSuperType)
@@ -110,13 +110,13 @@ let unify_r2l x = x
let sort_eqns = unify_r2l
*)
-let unify_0 env sigma cv_pb mod_delta m n =
- let trivial_unify pb substn m n =
- if (not(occur_meta m)) &&
- (if mod_delta then is_fconv (conv_pb_of pb) env sigma m n
- else eq_constr m n)
- then substn
- else error_cannot_unify env sigma (m,n) in
+let unify_0_with_initial_metas metas env sigma cv_pb mod_delta m n =
+ let trivial_unify pb (metasubst,_ as substn) m n =
+ match subst_defined_metas (* too strong: metasubst *) metas m with
+ | Some m when
+ (if mod_delta then is_fconv (conv_pb_of pb) env sigma m n
+ else eq_constr m n) -> substn
+ | _ -> error_cannot_unify env sigma (m,n) in
let rec unirec_rec curenv pb ((metasubst,evarsubst) as substn) curm curn =
let cM = Evarutil.whd_castappevar sigma curm
and cN = Evarutil.whd_castappevar sigma curn in
@@ -183,11 +183,13 @@ let unify_0 env sigma cv_pb mod_delta m n =
(if mod_delta then is_fconv (conv_pb_of cv_pb) env sigma m n
else eq_constr m n)
then
- ([],[])
+ (metas,[])
else
- let (mc,ec) = unirec_rec env cv_pb ([],[]) m n in
+ let (mc,ec) = unirec_rec env cv_pb (metas,[]) m n in
((*sort_eqns*) mc, (*sort_eqns*) ec)
+let unify_0 = unify_0_with_initial_metas []
+
let left = true
let right = false
@@ -229,11 +231,13 @@ let merge_instances env sigma mod_delta st1 st2 c1 c2 =
| (ConvUpToEta n1, ConvUpToEta n2) ->
let side = left (* arbitrary choice, but agrees with compatibility *) in
unify_with_eta side mod_delta env sigma n1 n2 c1 c2
- | ((IsSubType |ConvUpToEta _ as oppst1),(IsSubType |ConvUpToEta _)) ->
+ | ((IsSubType | ConvUpToEta _ | Coercible _ as oppst1),
+ (IsSubType | ConvUpToEta _ | Coercible _)) ->
let res = unify_0 env sigma Cumul mod_delta c2 c1 in
if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
else (st2=IsSubType, ConvUpToEta 0, res)
- | ((IsSuperType|ConvUpToEta _ as oppst1),(IsSuperType|ConvUpToEta _)) ->
+ | ((IsSuperType | ConvUpToEta _ | Coercible _ as oppst1),
+ (IsSuperType | ConvUpToEta _ | Coercible _)) ->
let res = unify_0 env sigma Cumul mod_delta c1 c2 in
if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
else (st2=IsSuperType, ConvUpToEta 0, res)
@@ -310,6 +314,15 @@ let is_mimick_head f =
match kind_of_term f with
(Const _|Var _|Rel _|Construct _|Ind _) -> true
| _ -> false
+
+let w_coerce env c ctyp target evd =
+ try
+ let j = make_judge c ctyp in
+ let tycon = mk_tycon_type target in
+ let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j tycon in
+ (evd',j'.uj_val)
+ with e when precatchable_exception e ->
+ evd,c
(* [w_merge env sigma b metas evars] merges common instances in metas
or in evars, possibly generating new unification problems; if [b]
@@ -365,19 +378,32 @@ let w_merge env with_types mod_delta metas evars evd =
w_merge_rec evd' (metas'@t) evars'
else
begin
+ let evd,n =
+ if with_types (* or occur_meta mvty *) then
+ let sigma = evars_of evd in
+ let metas = metas_of evd in
+ let mvty = Typing.meta_type evd mv in
+ let mvty = Tacred.hnf_constr env sigma mvty in
+ (* nf_betaiota was before in type_of - useful to reduce
+ types like (x:A)([x]P u) *)
+ let n = refresh_universes n in
+ let nty = get_type_of_with_meta env sigma metas n in
+ let nty = Tacred.hnf_constr env sigma (nf_betaiota nty) in
+ if occur_meta mvty then
+ (try
+ let (mc,ec) = unify_0 env sigma Cumul mod_delta nty mvty
+ in
+ ty_metas := mc @ !ty_metas;
+ ty_evars := ec @ !ty_evars;
+ evd,n
+ with e when precatchable_exception e -> evd,n)
+ else
+ (* Try to coerce to the type of [k]; cannot merge with the
+ previous case because Coercion does not handle Meta *)
+ w_coerce env n nty mvty evd
+ else
+ evd,n in
let evd' = meta_assign mv (n,status) evd in
- if with_types (* or occur_meta mvty *) then
- begin
- let mvty = Typing.meta_type evd' mv in
- try
- let sigma = evars_of evd' in
- let metas = metas_of evd' in
- let nty = get_type_of_with_meta env sigma metas (nf_meta evd' n) in
- let (mc,ec) = unify_0 env sigma Cumul mod_delta nty mvty in
- ty_metas := mc @ !ty_metas;
- ty_evars := ec @ !ty_evars
- with e when precatchable_exception e -> ()
- end;
w_merge_rec evd' t []
end
@@ -413,8 +439,10 @@ let w_merge env with_types mod_delta metas evars evd =
types of metavars are unifiable with the types of their instances *)
let w_unify_core_0 env with_types cv_pb mod_delta m n evd =
- let (mc,ec) = unify_0 env (evars_of evd) cv_pb mod_delta m n in
- w_merge env with_types mod_delta mc ec evd
+ let (mc1,evd') = retract_defined_metas evd in
+ let (mc2,ec) =
+ unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb mod_delta m n in
+ w_merge env with_types mod_delta mc2 ec evd'
let w_unify_0 env = w_unify_core_0 env false
let w_typed_unify env = w_unify_core_0 env true
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index c450bf622..aceba6e25 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -69,7 +69,7 @@ let e_constructor_tac boundopt i lbind gl =
| None -> ()
end;
let cons = mkConstruct (ith_constructor_of_inductive mind i) in
- let apply_tac = eapply_with_bindings (cons,lbind) in
+ let apply_tac = eapply_with_ebindings (cons,lbind) in
(tclTHENLIST [convert_concl_no_check redcl DEFAULTcast
; intros; apply_tac]) gl
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d46b6f142..8c8716110 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -81,7 +81,7 @@ let elimination_sort_of_clause = function
else back to the old approach
*)
-let general_rewrite_bindings_clause cls lft2rgt (c,l) with_evars gl =
+let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl =
let ctype = pf_apply get_type_of gl c in
(* A delta-reduction would be here too strong, since it would
break search for a defined setoid relation in head position. *)
@@ -111,13 +111,20 @@ let general_rewrite_bindings_clause cls lft2rgt (c,l) with_evars gl =
in
general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
-let general_rewrite_bindings = general_rewrite_bindings_clause None
-let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings) false
+let general_rewrite_ebindings =
+ general_rewrite_ebindings_clause None
+let general_rewrite_bindings l2r (c,bl) =
+ general_rewrite_ebindings_clause None l2r (c,inj_ebindings bl)
-let general_rewrite_bindings_in l2r id =
- general_rewrite_bindings_clause (Some id) l2r
+let general_rewrite l2r c =
+ general_rewrite_bindings l2r (c,NoBindings) false
+
+let general_rewrite_ebindings_in l2r id =
+ general_rewrite_ebindings_clause (Some id) l2r
+let general_rewrite_bindings_in l2r id (c,bl) =
+ general_rewrite_ebindings_clause (Some id) l2r (c,inj_ebindings bl)
let general_rewrite_in l2r id c =
- general_rewrite_bindings_clause (Some id) l2r (c,NoBindings)
+ general_rewrite_ebindings_clause (Some id) l2r (c,NoBindings)
let general_multi_rewrite l2r with_evars c cl =
if cl.concl_occs <> [] then
@@ -130,12 +137,12 @@ let general_multi_rewrite l2r with_evars c cl =
| [] -> tclIDTAC
| ((_,id),_) :: l ->
tclTHENFIRST
- (general_rewrite_bindings_in l2r id c with_evars)
+ (general_rewrite_ebindings_in l2r id c with_evars)
(do_hyps l)
in
if not cl.onconcl then do_hyps l else
tclTHENFIRST
- (general_rewrite_bindings l2r c with_evars)
+ (general_rewrite_ebindings l2r c with_evars)
(do_hyps l)
| None ->
(* Otherwise, if we are told to rewrite in all hypothesis via the
@@ -144,7 +151,7 @@ let general_multi_rewrite l2r with_evars c cl =
| [] -> (fun gl -> error "Nothing to rewrite.")
| id :: l ->
tclIFTHENTRYELSEMUST
- (general_rewrite_bindings_in l2r id c with_evars)
+ (general_rewrite_ebindings_in l2r id c with_evars)
(do_hyps_atleastonce l)
in
let do_hyps gl =
@@ -156,14 +163,14 @@ let general_multi_rewrite l2r with_evars c cl =
in
if not cl.onconcl then do_hyps else
tclIFTHENTRYELSEMUST
- (general_rewrite_bindings l2r c with_evars)
+ (general_rewrite_ebindings l2r c with_evars)
do_hyps
(* Conditional rewriting, the success of a rewriting is related
to the resolution of the conditions by a given tactic *)
let conditional_rewrite lft2rgt tac (c,bl) =
- tclTHENSFIRSTn (general_rewrite_bindings lft2rgt (c,bl) false)
+ tclTHENSFIRSTn (general_rewrite_ebindings lft2rgt (c,bl) false)
[|tclIDTAC|] (tclCOMPLETE tac)
let rewriteLR_bindings = general_rewrite_bindings true
@@ -176,7 +183,7 @@ let rewriteLRin_bindings = general_rewrite_bindings_in true
let rewriteRLin_bindings = general_rewrite_bindings_in false
let conditional_rewrite_in lft2rgt id tac (c,bl) =
- tclTHENSFIRSTn (general_rewrite_bindings_in lft2rgt id (c,bl) false)
+ tclTHENSFIRSTn (general_rewrite_ebindings_in lft2rgt id (c,bl) false)
[|tclIDTAC|] (tclCOMPLETE tac)
let rewriteRL_clause = function
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 9254e5f0d..36fc99594 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -26,7 +26,7 @@ open Genarg
(*i*)
val general_rewrite_bindings :
- bool -> constr with_ebindings -> evars_flag -> tactic
+ bool -> constr with_bindings -> evars_flag -> tactic
val general_rewrite :
bool -> constr -> tactic
@@ -42,7 +42,7 @@ val rewriteRL : constr -> tactic
(* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
val general_rewrite_bindings_in :
- bool -> identifier -> constr with_ebindings -> evars_flag -> tactic
+ bool -> identifier -> constr with_bindings -> evars_flag -> tactic
val general_rewrite_in :
bool -> identifier -> constr -> evars_flag -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ea33ead5d..d51d17aaf 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -323,7 +323,7 @@ let step left x tac =
let l =
List.map (fun lem ->
tclTHENLAST
- (apply_with_bindings (lem, ImplicitBindings [Evd.empty,x]))
+ (apply_with_bindings (lem, ImplicitBindings [x]))
tac)
!(if left then transitivity_left_table else transitivity_right_table)
in
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 85a85083e..b6c8f2ef8 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -41,7 +41,7 @@ let h_vm_cast_no_check c =
abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c)
let h_apply ev cb =
abstract_tactic (TacApply (ev,inj_open_wb cb))
- (apply_with_bindings_gen ev cb)
+ (apply_with_ebindings_gen ev cb)
let h_elim cb cbo =
abstract_tactic (TacElim (inj_open_wb cb,option_map inj_open_wb cbo))
(elim cb cbo)
@@ -96,9 +96,9 @@ let h_rename id1 id2 =
abstract_tactic (TacRename (id1,id2)) (rename_hyp id1 id2)
(* Constructors *)
-let h_left l = abstract_tactic (TacLeft l) (left l)
-let h_right l = abstract_tactic (TacLeft l) (right l)
-let h_split l = abstract_tactic (TacSplit (false,l)) (split l)
+let h_left l = abstract_tactic (TacLeft l) (left_with_ebindings l)
+let h_right l = abstract_tactic (TacLeft l) (right_with_ebindings l)
+let h_split l = abstract_tactic (TacSplit (false,l)) (split_with_ebindings l)
(* Moved to tacinterp because of dependence in Tacinterp.interp
let h_any_constructor t =
abstract_tactic (TacAnyConstructor t) (any_constructor t)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 47b8ca64b..6a9dc632b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -441,15 +441,14 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
tac
-let raw_inversion inv_kind indbinding id status names gl =
+let raw_inversion inv_kind id status names gl =
let env = pf_env gl and sigma = project gl in
let c = mkVar id in
let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in
let indclause = mk_clenv_from gl (c,t) in
- let indclause' = clenv_constrain_with_bindings indbinding indclause in
- let newc = clenv_value indclause' in
- let ccl = clenv_type indclause' in
- check_no_metas indclause' ccl;
+ let newc = clenv_value indclause in
+ let ccl = clenv_type indclause in
+ check_no_metas indclause ccl;
let IndType (indf,realargs) =
try find_rectype env sigma ccl
with Not_found ->
@@ -503,13 +502,13 @@ let wrap_inv_error id = function
| UserError ("Case analysis",s) -> errorlabstrm "Inv needs Nodep Prop Set" s
| UserError("mind_specif_of_mind",_) -> not_inductive_here id
| UserError (a,b) -> errorlabstrm "Inv" b
- | Invalid_argument (*"it_list2"*) "List.fold_left2" -> dep_prop_prop_message id
+ | Invalid_argument "List.fold_left2" -> dep_prop_prop_message id
| Not_found -> errorlabstrm "Inv" (not_found_message [id])
| e -> raise e
(* The most general inversion tactic *)
let inversion inv_kind status names id gls =
- try (raw_inversion inv_kind [] id status names) gls
+ try (raw_inversion inv_kind id status names) gls
with e -> wrap_inv_error id e
(* Specializing it... *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1b308e298..f34c9e38d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -292,7 +292,7 @@ let add_inversion_lemma_exn na com comsort bool tac =
let lemInv id c gls =
try
let clause = mk_clenv_type_of gls c in
- let clause = clenv_constrain_with_bindings [(-1,(Evd.empty,mkVar id))] clause in
+ let clause = clenv_constrain_last_binding (mkVar id) clause in
Clenvtac.res_pf clause ~allow_K:true gls
with
| UserError (a,b) ->
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 8fc95b408..1e70bf277 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1983,7 +1983,7 @@ let setoid_transitivity c gl =
| _ -> assert false
in
apply_with_bindings
- (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, (Evd.empty,c) ]) gl
+ (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
with
Optimize -> transitivity c gl
;;
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 4aad135c6..f13897d1f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -324,7 +324,7 @@ let general_elim_then_using
let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
(* applying elimination_scheme just a little modified *)
let indclause = mk_clenv_from gl (c,t) in
- let indclause' = clenv_constrain_with_bindings indbindings indclause in
+ let indclause' = clenv_match_args indbindings indclause in
let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in
let indmv =
match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
@@ -345,7 +345,7 @@ let general_elim_then_using
error ("The elimination combinator " ^ name_elim ^ " is not known")
in
let elimclause' = clenv_fchain indmv elimclause indclause' in
- let elimclause' = clenv_constrain_with_bindings elimbindings elimclause' in
+ let elimclause' = clenv_match_args elimbindings elimclause' in
let branchsigns = compute_construtor_signatures isrec ity in
let brnames = compute_induction_names (Array.length branchsigns) allnames in
let after_tac ce i gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b042a8422..8b10913de 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -55,6 +55,23 @@ let rec nb_prod x =
| _ -> n
in count 0 x
+let inj_open c = (Evd.empty,c)
+
+let inj_occ (occ,c) = (occ,inj_open c)
+
+let inj_red_expr = function
+ | Simpl lo -> Simpl (option_map inj_occ lo)
+ | Fold l -> Fold (List.map inj_open l)
+ | Pattern l -> Pattern (List.map inj_occ l)
+ | (ExtraRedExpr _ | CbvVm | Red _ | Hnf | Cbv _ | Lazy _ | Unfold _ as c)
+ -> c
+
+let inj_ebindings = function
+ | NoBindings -> NoBindings
+ | ImplicitBindings l -> ImplicitBindings (List.map inj_open l)
+ | ExplicitBindings l ->
+ ExplicitBindings (List.map (fun (l,id,c) -> (l,id,inj_open c)) l)
+
(*********************************************)
(* Tactics *)
(*********************************************)
@@ -527,7 +544,7 @@ let clenv_refine_in with_evars id clenv gl =
(* Resolution with missing arguments *)
-let apply_with_bindings_gen with_evars (c,lbind) gl =
+let apply_with_ebindings_gen with_evars (c,lbind) gl =
(* The actual type of the theorem. It will be matched against the
goal. If this fails, then the head constant will be unfolded step by
step. *)
@@ -553,24 +570,20 @@ let apply_with_bindings_gen with_evars (c,lbind) gl =
else Clenvtac.res_pf clause gl in
try_apply thm_ty0
-let apply_with_bindings = apply_with_bindings_gen false
-let eapply_with_bindings = apply_with_bindings_gen true
+let apply_with_ebindings = apply_with_ebindings_gen false
+let eapply_with_ebindings = apply_with_ebindings_gen true
-let apply c = apply_with_bindings (c,NoBindings)
+let apply_with_bindings (c,bl) =
+ apply_with_ebindings (c,inj_ebindings bl)
-let inj_open c = (Evd.empty,c)
-
-let inj_occ (occ,c) = (occ,inj_open c)
+let eapply_with_bindings (c,bl) =
+ apply_with_ebindings_gen true (c,inj_ebindings bl)
-let inj_red_expr = function
- | Simpl lo -> Simpl (option_map inj_occ lo)
- | Fold l -> Fold (List.map inj_open l)
- | Pattern l -> Pattern (List.map inj_occ l)
- | (ExtraRedExpr _ | CbvVm | Red _ | Hnf | Cbv _ | Lazy _ | Unfold _ as c)
- -> c
+let apply c =
+ apply_with_ebindings (c,NoBindings)
let apply_list = function
- | c::l -> apply_with_bindings (c,ImplicitBindings (List.map inj_open l))
+ | c::l -> apply_with_bindings (c,ImplicitBindings l)
| _ -> assert false
(* Resolution with no reduction on the type *)
@@ -713,6 +726,7 @@ let rec intros_clearing = function
let new_hyp mopt (c,lbind) g =
let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
+ let clause = clenv_unify_meta_types clause in
let (thd,tstack) = whd_stack (clenv_value clause) in
let nargs = List.length tstack in
let cut_pf =
@@ -720,7 +734,10 @@ let new_hyp mopt (c,lbind) g =
match mopt with
| Some m -> if m < nargs then list_firstn m tstack else tstack
| None -> tstack)
- in
+ in
+ if occur_meta cut_pf then
+ errorlabstrm "" (str "Cannot infer an instance for " ++
+ pr_name (meta_name clause.evd (List.hd (collect_metas cut_pf))));
(tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.evd))
(cut (pf_type_of g cut_pf)))
((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
@@ -744,21 +761,24 @@ let keep hyps gl =
(* Introduction tactics *)
(************************)
-let constructor_tac boundopt i lbind gl =
+let check_number_of_constructors expctdnumopt i nconstr =
+ if i=0 then error "The constructors are numbered starting from 1";
+ begin match expctdnumopt with
+ | Some n when n <> nconstr ->
+ error ("Not an inductive goal with "^
+ string_of_int n^plural n " constructor")
+ | _ -> ()
+ end;
+ if i > nconstr then error "Not enough constructors"
+
+let constructor_tac expctdnumopt i lbind gl =
let cl = pf_concl gl in
let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in
let nconstr =
Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
- if i=0 then error "The constructors are numbered starting from 1";
- if i > nconstr then error "Not enough constructors";
- begin match boundopt with
- | Some expctdnum ->
- if expctdnum <> nconstr then
- error "Not the expected number of constructors"
- | None -> ()
- end;
+ check_number_of_constructors expctdnumopt i nconstr;
let cons = mkConstruct (ith_constructor_of_inductive mind i) in
- let apply_tac = apply_with_bindings (cons,lbind) in
+ let apply_tac = apply_with_ebindings (cons,lbind) in
(tclTHENLIST
[convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
@@ -778,15 +798,20 @@ let any_constructor tacopt gl =
tclFIRST (List.map (fun i -> tclTHEN (one_constructor i NoBindings) t)
(interval 1 nconstr)) gl
-let left = constructor_tac (Some 2) 1
+let left_with_ebindings = constructor_tac (Some 2) 1
+let right_with_ebindings = constructor_tac (Some 2) 2
+let split_with_ebindings = constructor_tac (Some 1) 1
+
+let left l = left_with_ebindings (inj_ebindings l)
let simplest_left = left NoBindings
-let right = constructor_tac (Some 2) 2
+let right l = right_with_ebindings (inj_ebindings l)
let simplest_right = right NoBindings
-let split = constructor_tac (Some 1) 1
+let split l = split_with_ebindings (inj_ebindings l)
let simplest_split = split NoBindings
+
(********************************************)
(* Elimination tactics *)
(********************************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6b0f8413a..0c2024162 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -30,6 +30,7 @@ open Rawterm
val inj_open : constr -> open_constr
val inj_red_expr : red_expr -> (open_constr, evaluable_global_reference) red_expr_gen
+val inj_ebindings : constr bindings -> open_constr bindings
(* Main tactics. *)
@@ -169,9 +170,11 @@ val bring_hyps : named_context -> tactic
val apply : constr -> tactic
val apply_without_reduce : constr -> tactic
val apply_list : constr list -> tactic
-val apply_with_bindings_gen : evars_flag -> constr with_ebindings -> tactic
-val apply_with_bindings : constr with_ebindings -> tactic
-val eapply_with_bindings : constr with_ebindings -> tactic
+val apply_with_ebindings_gen : evars_flag -> constr with_ebindings -> tactic
+val apply_with_bindings : constr with_bindings -> tactic
+val apply_with_ebindings : constr with_ebindings -> tactic
+val eapply_with_bindings : constr with_bindings -> tactic
+val eapply_with_ebindings : constr with_ebindings -> tactic
val cut_and_apply : constr -> tactic
@@ -271,11 +274,17 @@ val constructor_tac : int option -> int ->
open_constr bindings -> tactic
val one_constructor : int -> open_constr bindings -> tactic
val any_constructor : tactic option -> tactic
-val left : open_constr bindings -> tactic
+
+val left : constr bindings -> tactic
+val right : constr bindings -> tactic
+val split : constr bindings -> tactic
+
+val left_with_ebindings : open_constr bindings -> tactic
+val right_with_ebindings : open_constr bindings -> tactic
+val split_with_ebindings : open_constr bindings -> tactic
+
val simplest_left : tactic
-val right : open_constr bindings -> tactic
val simplest_right : tactic
-val split : open_constr bindings -> tactic
val simplest_split : tactic
(*s Logical connective tactics. *)
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 3c9fbeb36..fb6250d50 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -28,3 +28,68 @@ Notation S':=S (only parsing).
Goal (forall S, S = S' S) -> (forall S, S = S' S).
intros.
apply H with (S0 := S).
+
+(* Check inference of implicit arguments in bindings *)
+
+Goal exists y : nat -> Type, y 0 = y 0.
+exists (fun x => True).
+trivial.
+Qed.
+
+(* Check universe handling in typed unificationn *)
+
+Definition E := Type.
+Goal exists y : E, y = y.
+exists Prop.
+trivial.
+Qed.
+
+Definition E := Type.
+Variable Eq : Prop = (Prop -> Prop) :> E.
+Goal Prop.
+rewrite Eq.
+Abort.
+
+(* Check insertion of coercions in bindings *)
+
+Coercion eq_true : bool >-> Sortclass.
+Goal exists A:Prop, A = A.
+exists true.
+trivial.
+Qed.
+
+(* Check use of unification of bindings types in specialize *)
+
+Variable P : nat -> Prop.
+Variable L : forall (l : nat), P l -> P l.
+Goal P 0 -> True.
+intros.
+specialize L with (1:=H).
+Abort.
+Reset P.
+
+(* Two examples that show that hnf_constr is used when unifying types
+ of bindings *)
+
+Require Import List.
+Open Scope list_scope.
+Fixpoint P (l : list nat) : Prop :=
+ match l with
+ | nil => True
+ | e1 :: nil => e1 = e1
+ | e1 :: l1 => e1 = e1 /\ P l1
+ end.
+Variable L : forall n l, P (n::l) -> P l.
+
+Goal forall (x:nat) l, P (x::l) -> P l.
+intros.
+apply L with (1:=H).
+Qed.
+
+Goal forall (x:nat) l, match l with nil => x=x | _::_ => x=x /\ P l end -> P l.
+intros.
+apply L with (1:=H).
+Qed.
+
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 14:47:16 +0000