aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/term.ml1
-rw-r--r--kernel/term.mli1
-rw-r--r--pretyping/clenv.ml91
-rw-r--r--pretyping/clenv.mli8
-rw-r--r--pretyping/evd.ml6
-rw-r--r--pretyping/evd.mli4
-rw-r--r--pretyping/reductionops.ml55
-rw-r--r--pretyping/reductionops.mli1
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/termops.ml4
-rw-r--r--pretyping/termops.mli7
-rw-r--r--pretyping/unification.ml2
-rw-r--r--proofs/clenvtac.ml25
-rw-r--r--proofs/logic.ml4
-rw-r--r--proofs/refiner.mli2
-rw-r--r--proofs/tacmach.mli2
-rw-r--r--tactics/auto.ml6
-rw-r--r--tactics/class_tactics.ml421
-rw-r--r--tactics/decl_proof_instr.mli5
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/refine.ml2
-rw-r--r--tactics/setoid_replace.ml2
-rw-r--r--tactics/tacinterp.ml8
-rw-r--r--tactics/tactics.ml14
-rw-r--r--tactics/tactics.mli3
25 files changed, 170 insertions, 108 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index d274857af..49d7afa22 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -261,6 +261,7 @@ let mkFix fix = Fix fix
let mkCoFix cofix = CoFix cofix
let kind_of_term c = c
+let kind_of_term2 c = c
(************************************************************************)
(* kind_of_term = constructions as seen by the user *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 2ab03e50f..5d75df4bf 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -208,6 +208,7 @@ type ('constr, 'types) kind_of_term =
term *)
val kind_of_term : constr -> (constr, types) kind_of_term
+val kind_of_term2 : constr -> ((constr,types) kind_of_term,constr) kind_of_term
(* Experimental *)
type ('constr, 'types) kind_of_type =
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 732ff1e69..c5c246877 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -54,11 +54,77 @@ let subst_clenv sub clenv =
env = clenv.env }
let clenv_nf_meta clenv c = nf_meta clenv.evd c
+let clenv_direct_nf_meta clenv c = direct_nf_meta clenv.evd c
let clenv_term clenv c = meta_instance clenv.evd c
let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
let clenv_value clenv = meta_instance clenv.evd clenv.templval
+let clenv_direct_value clenv = nf_betaiota clenv.templval.rebus
let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
-
+let clenv_direct_nf_type clenv = nf_betaiota clenv.templtyp.rebus
+
+let plain_instance find c =
+ let rec irec u = match kind_of_term u with
+ | Meta p -> find p
+ | App (f,l) when isCast f ->
+ let (f,_,t) = destCast f in
+ let l' = Array.map irec l in
+ (match kind_of_term f with
+ | Meta p ->
+ (* Don't flatten application nodes: this is used to extract a
+ proof-term from a proof-tree and we want to keep the structure
+ of the proof-tree *)
+ let g = find p in
+ (match kind_of_term g with
+ | App _ ->
+ let h = id_of_string "H" in
+ mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
+ | _ -> mkApp (g,l'))
+ | _ -> mkApp (irec f,l'))
+ | Cast (m,_,_) when isMeta m -> find (destMeta m)
+ | _ -> map_constr irec u
+ in
+ local_strong whd_betaiota
+ (if c.freemetas = Metaset.empty then c.rebus else irec c.rebus)
+
+let clenv_expand_metas clenv =
+ let seen = ref Metamap.empty in
+ let ongoing = ref Metaset.empty in
+ let todo = ref (meta_list clenv.evd) in
+
+ let rec process_all () = match !todo with
+ | [] -> ()
+ | (mv,cl)::_ -> let _ = process_meta mv cl in process_all ()
+
+ and process_meta mv cl =
+ ongoing := Metaset.add mv !ongoing;
+ let (body,typ) = match cl with
+ | Clval (na,(body,status),typ) ->
+ let body = plain_instance instance_of_meta body in
+ let typ = plain_instance instance_of_meta typ in
+ (body,Clval(na,(mk_freelisted body,status),mk_freelisted typ))
+ | Cltyp (na,typ) ->
+ let typ = plain_instance instance_of_meta typ in
+ (mkMeta mv,Cltyp(na,mk_freelisted typ)) in
+ ongoing := Metaset.remove mv !ongoing;
+ seen := Metamap.add mv (body,typ) !seen;
+ todo := List.remove_assoc mv !todo;
+ body
+
+ and instance_of_meta mv =
+ try fst (Metamap.find mv !seen)
+ with Not_found ->
+ if Metaset.mem mv !ongoing then
+ error "Cannot instantiate an existential variable with a term which depends on itself";
+ process_meta mv (find_meta clenv.evd mv) in
+
+ process_all ();
+
+ { clenv with
+ evd = replace_metas (Metamap.map snd !seen) clenv.evd;
+ templtyp = mk_freelisted(plain_instance instance_of_meta clenv.templtyp);
+ templval = mk_freelisted(plain_instance instance_of_meta clenv.templval)}
+
+let instantiated_clenv_template clenv = (clenv.templval,clenv.templtyp)
let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
@@ -68,7 +134,8 @@ let clenv_get_type_of ce c =
exception NotExtensibleClause
let clenv_push_prod cl =
- let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+ let typ =
+ whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_direct_nf_type cl) in
let rec clrec typ = match kind_of_term typ with
| Cast (t,_,_) -> clrec t
| Prod (na,t,u) ->
@@ -213,13 +280,9 @@ let clenv_wtactic f clenv = {clenv with evd = f clenv.evd }
* returns a list of the metavars which appear in the type of
* the metavar mv. The list is unordered. *)
-let clenv_metavars evd mv =
- (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
-
let dependent_metas clenv mvs conclmetas =
List.fold_right
- (fun mv deps ->
- Metaset.union deps (clenv_metavars clenv.evd mv))
+ (fun mv deps -> Metaset.union deps (meta_ftype clenv.evd mv).freemetas)
mvs conclmetas
let duplicated_metas c =
@@ -231,14 +294,14 @@ let duplicated_metas c =
snd (collrec ([],[]) c)
let clenv_dependent hyps_only clenv =
+ let (body,typ) = instantiated_clenv_template clenv in
let mvs = undefined_metas clenv.evd in
- let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
- let deps = dependent_metas clenv mvs ctyp_mvs in
- let nonlinear = duplicated_metas (clenv_value clenv) in
+ let deps = dependent_metas clenv mvs typ.freemetas in
+ let nonlinear = duplicated_metas body.rebus in
(* Make the assumption that duplicated metas have internal dependencies *)
List.filter
(fun mv -> (Metaset.mem mv deps &&
- not (hyps_only && Metaset.mem mv ctyp_mvs))
+ not (hyps_only && Metaset.mem mv typ.freemetas))
or List.mem mv nonlinear)
mvs
@@ -367,9 +430,9 @@ type arg_bindings = open_constr explicit_bindings
* of cval, ctyp. *)
let clenv_independent clenv =
- let mvs = collect_metas (clenv_value clenv) in
- let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
- let deps = dependent_metas clenv mvs ctyp_mvs in
+ let (body,typ) = instantiated_clenv_template clenv in
+ let mvs = Metaset.elements body.freemetas in
+ let deps = dependent_metas clenv mvs typ.freemetas in
List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
let check_bindings bl =
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index dfa751349..de5a1e375 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -43,10 +43,16 @@ val subst_clenv : substitution -> clausenv -> clausenv
(* subject of clenv (instantiated) *)
val clenv_value : clausenv -> constr
+(* subject of clenv (assume it is pre-instantiated) *)
+val clenv_direct_value : clausenv -> constr
(* type of clenv (instantiated) *)
val clenv_type : clausenv -> types
+(* type of clenv (assume it is pre-instantiated) *)
+val clenv_direct_nf_type : clausenv -> types
(* substitute resolved metas *)
val clenv_nf_meta : clausenv -> constr -> constr
+(* substitute resolved metas (assume the metas in clausenv are expanded) *)
+val clenv_direct_nf_meta : clausenv -> constr -> constr
(* type of a meta in clenv context *)
val clenv_meta_type : clausenv -> metavariable -> types
@@ -83,6 +89,8 @@ val clenv_dependent : bool -> clausenv -> metavariable list
val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
+val clenv_expand_metas : clausenv -> clausenv
+
(***************************************************************)
(* Bindings *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index b29afc0cb..2b9a0ed82 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -610,12 +610,18 @@ let meta_with_name evd id =
(str "Binder name \"" ++ pr_id id ++
strbrk "\" occurs more than once in clause.")
+let mk_meta_subst evd =
+ Metamap.fold (fun mv cl subst -> match cl with
+ | Clval(_,(b,_),typ) -> (mv, b.rebus) :: subst
+ | Cltyp (_,typ) -> subst) evd.metas []
let meta_merge evd1 evd2 =
{evd2 with
metas = List.fold_left (fun m (n,v) -> Metamap.add n v m)
evd2.metas (metamap_to_list evd1.metas) }
+let replace_metas metas evd = { evd with metas = metas }
+
type metabinding = metavariable * constr * instance_status
let retract_coercible_metas evd =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 38db90dad..2fd668043 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -218,13 +218,15 @@ val meta_declare :
metavariable -> types -> ?name:name -> evar_defs -> evar_defs
val meta_assign : metavariable -> constr * instance_status -> evar_defs -> evar_defs
val meta_reassign : metavariable -> constr * instance_status -> evar_defs -> evar_defs
+val mk_meta_subst : evar_defs -> meta_value_map
(* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
val meta_merge : evar_defs -> evar_defs -> evar_defs
val undefined_metas : evar_defs -> metavariable list
-val metas_of : evar_defs -> metamap
+val metas_of : evar_defs -> meta_type_map
val map_metas_fvalue : (constr -> constr) -> evar_defs -> evar_defs
+val replace_metas : clbinding Metamap.t -> evar_defs -> evar_defs
type metabinding = metavariable * constr * instance_status
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 57af582a1..e3553ddd6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -130,15 +130,15 @@ type local_state_reduction_function = state -> state
(*** Reduction Functions Operators ***)
(*************************************)
-let rec whd_state (x, stack as s) =
+let rec whd_app_state (x, stack as s) =
match kind_of_term x with
- | App (f,cl) -> whd_state (f, append_stack cl stack)
- | Cast (c,_,_) -> whd_state (c, stack)
+ | App (f,cl) -> whd_app_state (f, append_stack cl stack)
+ | Cast (c,_,_) -> whd_app_state (c, stack)
| _ -> s
let appterm_of_stack (f,s) = (f,list_of_stack s)
-let whd_stack x = appterm_of_stack (whd_state (x, empty_stack))
+let whd_stack x = appterm_of_stack (whd_app_state (x, empty_stack))
let whd_castapp_stack = whd_stack
let stack_reduction_of_reduction red_fun env sigma s =
@@ -185,26 +185,6 @@ module type RedFlagsSig = sig
val red_zeta : flags -> bool
end
-(* Naive Implementation
-module RedFlags = (struct
- type flag = BETA | DELTA | EVAR | IOTA | ZETA | ETA
- type flags = flag list
- let fbeta = BETA
- let fdelta = DELTA
- let fevar = EVAR
- let fiota = IOTA
- let fzeta = ZETA
- let feta = ETA
- let mkflags l = l
- let red_beta = List.mem BETA
- let red_delta = List.mem DELTA
- let red_evar = List.mem EVAR
- let red_eta = List.mem ETA
- let red_iota = List.mem IOTA
- let red_zeta = List.mem ZETA
-end : RedFlagsSig)
-*)
-
(* Compact Implementation *)
module RedFlags = (struct
type flag = int
@@ -531,14 +511,14 @@ let rec whd_evar sigma c =
with NotInstantiatedEvar | Not_found -> None in
(match d with Some c -> whd_evar sigma c | None -> c)
| Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
- | _ -> collapse_appl c
+ | _ -> c
let nf_evar sigma =
local_strong (whd_evar sigma)
(* lazy reduction functions. The infos must be created for each term *)
let clos_norm_flags flgs env sigma t =
- norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t))
+ norm_val (create_clos_infos flgs env) (inject ((*nf_evar sigma *)t))
let nf_beta = clos_norm_flags Closure.beta empty_env Evd.empty
let nf_betaiota = clos_norm_flags Closure.betaiota empty_env Evd.empty
@@ -645,8 +625,8 @@ let is_trans_fconv = function | CONV -> is_trans_conv | CUMUL -> is_trans_conv_l
(* Special-Purpose Reduction *)
(********************************************************************)
-let whd_meta metamap c = match kind_of_term c with
- | Meta p -> (try List.assoc p metamap with Not_found -> c)
+let whd_meta metasubst c = match kind_of_term c with
+ | Meta p -> (try List.assoc p metasubst with Not_found -> c)
| _ -> c
(* Try to replace all metas. Does not replace metas in the metas' values
@@ -905,27 +885,18 @@ let meta_value evd mv =
in
valrec mv
-let meta_instance env b =
+let meta_instance evd b =
let c_sigma =
List.map
- (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
+ (fun mv -> (mv,meta_value evd mv)) (Metaset.elements b.freemetas)
in
if c_sigma = [] then b.rebus else instance c_sigma b.rebus
-let nf_meta env c = meta_instance env (mk_freelisted c)
+let nf_meta evd c = meta_instance evd (mk_freelisted c)
-(* Instantiate metas that create beta/iota redexes *)
+let direct_nf_meta evd c = instance (mk_meta_subst evd) c
-let meta_value evd mv =
- let rec valrec mv =
- match meta_opt_fvalue evd mv with
- | Some (b,_) ->
- instance
- (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
- b.rebus
- | None -> mkMeta mv
- in
- valrec mv
+(* Instantiate metas that create beta/iota redexes *)
let meta_reducible_instance evd b =
let fm = Metaset.elements b.freemetas in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 371a66a9d..397377473 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -223,4 +223,5 @@ val whd_betaiota_deltazeta_for_iota_state : state_reduction_function
(*s Meta-related reduction functions *)
val meta_instance : evar_defs -> constr freelisted -> constr
val nf_meta : evar_defs -> constr -> constr
+val direct_nf_meta : evar_defs -> constr -> constr
val meta_reducible_instance : evar_defs -> constr freelisted -> constr
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index c7901e949..52e5d7049 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -26,7 +26,7 @@ val get_sort_of : env -> evar_map -> types -> sorts
val get_sort_family_of : env -> evar_map -> types -> sorts_family
val get_type_of_with_meta :
- env -> evar_map -> Termops.metamap -> constr -> types
+ env -> evar_map -> Termops.meta_type_map -> constr -> types
(* Makes an assumption from a constr *)
val get_assumption_of : env -> evar_map -> constr -> types
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 7cbde2d07..a77fc5741 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -555,7 +555,9 @@ let pop t = lift (-1) t
(* bindings functions *)
(***************************)
-type metamap = (metavariable * constr) list
+type meta_type_map = (metavariable * types) list
+
+type meta_value_map = (metavariable * constr) list
let rec subst_meta bl c =
match kind_of_term c with
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 15751b91c..e9516ec48 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -105,8 +105,11 @@ 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
+type meta_value_map = (metavariable * constr) list
+val subst_meta : meta_value_map -> constr -> constr
+
+(* Type assignment for metavariables *)
+type meta_type_map = (metavariable * types) list
(* [pop c] lifts by -1 the positive indexes in [c] *)
val pop : constr -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a2671b5d1..a18db9026 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -467,7 +467,7 @@ let unify_to_type env evd flags c u =
let sigma = evars_of evd in
let c = refresh_universes c in
let t = get_type_of_with_meta env sigma (metas_of evd) c in
- let t = Tacred.hnf_constr env sigma (nf_betaiota (nf_meta evd t)) in
+ let t = Tacred.hnf_constr env sigma (nf_meta evd t) in
let u = Tacred.hnf_constr env sigma u in
try unify_0 env sigma Cumul flags t u
with e when precatchable_exception e -> ([],[])
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 624b671d3..5c204c8bb 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -40,28 +40,30 @@ open Clenv
let clenv_cast_meta clenv =
let rec crec u =
- match kind_of_term u with
+ match kind_of_term2 u with
| App _ | Case _ -> crec_hd u
- | Cast (c,_,_) when isMeta c -> u
+ | Cast (Meta mv,_,_) | Meta mv ->
+ (match Evd.meta_opt_fvalue clenv.evd mv with
+ | Some (c,_) -> c.rebus
+ | None -> u)
| _ -> map_constr crec u
and crec_hd u =
match kind_of_term (strip_outer_cast u) with
| Meta mv ->
- (try
- let b = Typing.meta_type clenv.evd mv in
- if occur_meta b then u
- else mkCast (mkMeta mv, DEFAULTcast, b)
- with Not_found -> u)
+ (match Evd.find_meta clenv.evd mv with
+ | Clval (_,(body,_),_) -> body.rebus
+ | Cltyp (_,typ) ->
+ assert (not (occur_meta typ.rebus));
+ mkCast (mkMeta mv, DEFAULTcast, typ.rebus))
| App(f,args) -> mkApp (crec_hd f, Array.map crec args)
- | Case(ci,p,c,br) ->
- mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
+ | Case(ci,p,c,br) -> mkCase (ci, crec p, crec_hd c, Array.map crec br)
| _ -> u
in
crec
let clenv_value_cast_meta clenv =
- clenv_cast_meta clenv (clenv_value clenv)
+ clenv_cast_meta clenv (clenv_direct_value clenv)
let clenv_pose_dependent_evars with_evars clenv =
let dep_mvs = clenv_dependent false clenv in
@@ -72,10 +74,11 @@ let clenv_pose_dependent_evars with_evars clenv =
let clenv_refine with_evars clenv gls =
+ let clenv = clenv_expand_metas clenv in
let clenv = clenv_pose_dependent_evars with_evars clenv in
tclTHEN
(tclEVARS (evars_of clenv.evd))
- (refine (clenv_cast_meta clenv (clenv_value clenv)))
+ (refine (clenv_value_cast_meta clenv))
gls
let dft = Unification.default_unify_flags
diff --git a/proofs/logic.ml b/proofs/logic.ml
index eb879d977..c358de9ba 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -251,7 +251,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
match kind_of_term trm with
| Meta _ ->
if !check && occur_meta conclty then
- anomaly "refined called with a dependent meta";
+ anomaly "refine called with a dependent meta";
(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
| Cast (t,_, ty) ->
@@ -329,7 +329,7 @@ and mk_hdgoals sigma goal goalacc trm =
| _ ->
if !check && occur_meta trm then
- anomaly "refined called with a dependent meta";
+ anomaly "refine called with a dependent meta";
goalacc, goal_type_of env sigma trm
and mk_arggoals sigma goal goalacc funty = function
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 6d5f26bae..f6ebcae66 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -205,7 +205,7 @@ val weak_undo_pftreestate : pftreestate -> pftreestate
val mk_pftreestate : goal -> pftreestate
val extract_open_proof : evar_map -> proof_tree -> constr * (int * types) list
-val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
+val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map
val extract_pftreestate : pftreestate -> constr
val first_unproven : pftreestate -> pftreestate
val last_unproven : pftreestate -> pftreestate
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index d9a89329a..a73e79a0c 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -106,7 +106,7 @@ val weak_undo_pftreestate : pftreestate -> pftreestate
val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate
val solve_pftreestate : tactic -> pftreestate -> pftreestate
val mk_pftreestate : goal -> pftreestate
-val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
+val extract_open_pftreestate : pftreestate -> constr * Termops.meta_type_map
val extract_pftreestate : pftreestate -> constr
val first_unproven : pftreestate -> pftreestate
val last_unproven : pftreestate -> pftreestate
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 58730d5d1..e9ec90ec3 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -264,7 +264,7 @@ let make_exact_entry pri (c,cty) =
failwith "make_exact_entry"
| _ ->
let ce = mk_clenv_from dummy_goal (c,cty) in
- let c' = clenv_type ce in
+ let c' = clenv_direct_nf_type ce in
let pat = Pattern.pattern_of_constr c' in
(Some (head_of_constr_reference (List.hd (head_constr cty))),
{ pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
@@ -274,7 +274,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
match kind_of_term cty with
| Prod _ ->
let ce = mk_clenv_from dummy_goal (c,cty) in
- let c' = clenv_type ce in
+ let c' = clenv_direct_nf_type ce in
let pat = Pattern.pattern_of_constr c' in
let hd = (try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry") in
@@ -342,7 +342,7 @@ let make_trivial env sigma c =
let hd = head_of_constr_reference (List.hd (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 (clenv_direct_nf_type ce));
code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
open Vernacexpr
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e9bd15b11..c7cebd110 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -751,7 +751,7 @@ let evd_convertible env evd x y =
let decompose_setoid_eqhyp env sigma c left2right =
let ctype = Typing.type_of env sigma c in
let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ctype) in
- let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
+ let (equiv, args) = decompose_app (Clenv.clenv_direct_nf_type eqclause) in
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z ->
@@ -764,7 +764,7 @@ let decompose_setoid_eqhyp env sigma c left2right =
if not (evd_convertible env eqclause.evd ty1 ty2) then
error "The term does not end with an applied homogeneous relation."
else
- { cl=eqclause; prf=(Clenv.clenv_value eqclause);
+ { cl=eqclause; prf=(Clenv.clenv_direct_value eqclause);
car=ty1; rel=mkApp (equiv, Array.of_list others);
l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
@@ -808,6 +808,7 @@ let unify_eqn env sigma hypinfo t =
cl, prf, c1, c2, car, rel
else raise Not_found*)
let env' = clenv_unify allowK ~flags:rewrite2_unif_flags CONV left t cl in
+ let env' = clenv_expand_metas env' in
let env' =
let mvs = clenv_dependent false env' in
clenv_pose_metas_as_evars env' mvs
@@ -818,7 +819,8 @@ let unify_eqn env sigma hypinfo t =
and rel = Clenv.clenv_nf_meta env' rel in
hypinfo := { !hypinfo with
cl = env';
- abs = Some (Clenv.clenv_value env', Clenv.clenv_type env') };
+ abs = Some (Clenv.clenv_direct_value env',
+ Clenv.clenv_direct_nf_type env') };
env', prf, c1, c2, car, rel
| None ->
let env' =
@@ -829,6 +831,7 @@ let unify_eqn env sigma hypinfo t =
clenv_unify allowK ~flags:rewrite2_unif_flags
CONV left t cl
in
+ let env' = clenv_expand_metas env' in
let env' =
let mvs = clenv_dependent false env' in
clenv_pose_metas_as_evars env' mvs
@@ -838,7 +841,7 @@ let unify_eqn env sigma hypinfo t =
let nf c = Evarutil.nf_evar (Evd.evars_of evd') (Clenv.clenv_nf_meta env' c) in
let c1 = nf c1 and c2 = nf c2
and car = nf car and rel = nf rel
- and prf = nf (Clenv.clenv_value env') in
+ and prf = nf (Clenv.clenv_direct_value env') in
let ty1 = Typing.mtype_of env'.env env'.evd c1
and ty2 = Typing.mtype_of env'.env env'.evd c2
in
@@ -1577,12 +1580,12 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
Unification.w_unify_to_subterm ~flags:rewrite2_unif_flags
(pf_env gl) ((if l2r then c1 else c2),but) cl.evd
in
- let cl' = {cl with evd = env'} in
- let c1 = Clenv.clenv_nf_meta cl' c1
- and c2 = Clenv.clenv_nf_meta cl' c2 in
+ let cl' = clenv_expand_metas {cl with evd = env'} in
+ let c1 = Clenv.clenv_direct_nf_meta cl' c1
+ and c2 = Clenv.clenv_direct_nf_meta cl' c2 in
check_evar_map_of_evars_defs env';
- let prf = Clenv.clenv_value cl' in
- let prfty = Clenv.clenv_type cl' in
+ let prf = Clenv.clenv_direct_value cl' in
+ let prfty = Clenv.clenv_direct_nf_type cl' in
let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in
{cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli
index 5777d6af8..fa1a703b9 100644
--- a/tactics/decl_proof_instr.mli
+++ b/tactics/decl_proof_instr.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id:$ *)
+(* $Id$ *)
open Refiner
open Names
@@ -23,7 +23,8 @@ val automation_tac : tactic
val daimon_subtree: pftreestate -> pftreestate
-val concl_refiner: Termops.metamap -> constr -> Proof_type.goal sigma -> constr
+val concl_refiner:
+ Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr
val do_instr: Decl_expr.raw_proof_instr -> pftreestate -> pftreestate
val proof_instr: Decl_expr.raw_proof_instr -> unit
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9994bd784..123c83e40 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -565,7 +565,7 @@ let apply_on_clause (f,t) clause =
(match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
| Meta mv -> mv
| _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
- clenv_fchain argmv f_clause clause
+ clenv_expand_metas (clenv_fchain argmv f_clause clause)
let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
let e = next_ident_away eq_baseid (ids_of_context env) in
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 39567f981..c0db5def5 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -60,7 +60,7 @@ open Tactics
open Tacticals
open Printer
-type term_with_holes = TH of constr * metamap * sg_proofs
+type term_with_holes = TH of constr * meta_type_map * sg_proofs
and sg_proofs = (term_with_holes option) list
(* pour debugger *)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 644a68666..22596ac3c 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1815,7 +1815,7 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
let analyse_hypothesis gl c =
let ctype = pf_type_of gl c in
let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
- let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
+ let (equiv, args) = decompose_app (Clenv.clenv_direct_nf_type eqclause) in
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c40d40208..72500c7e3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -486,7 +486,9 @@ let rec intern_intro_pattern lf ist = function
loc, IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
| loc, IntroIdentifier id ->
loc, IntroIdentifier (intern_ident lf ist id)
- | loc, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _)
+ | loc, IntroFresh id ->
+ loc, IntroFresh (intern_ident lf ist id)
+ | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _)
as x -> x
and intern_or_and_intro_pattern lf ist =
@@ -1644,7 +1646,9 @@ let rec interp_intro_pattern ist gl = function
loc, IntroOrAndPattern (interp_or_and_intro_pattern ist gl l)
| loc, IntroIdentifier id ->
loc, interp_intro_pattern_var loc ist (pf_env gl) id
- | loc, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _)
+ | loc, IntroFresh id ->
+ loc, IntroFresh (interp_fresh_ident ist gl id)
+ | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _)
as x -> x
and interp_or_and_intro_pattern ist gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 02d9544f0..65082c2ee 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -560,11 +560,12 @@ let error_uninstantiated_metas t clenv =
in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
let clenv_refine_in with_evars id clenv gl =
+ let clenv = clenv_expand_metas clenv in
let clenv = clenv_pose_dependent_evars with_evars clenv in
- let new_hyp_typ = clenv_type clenv in
+ let new_hyp_typ = clenv_type clenv in
if not with_evars & occur_meta new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
- let new_hyp_prf = clenv_value clenv in
+ let new_hyp_prf = clenv_value_cast_meta clenv in
tclTHEN
(tclEVARS (evars_of clenv.evd))
(cut_replacing id new_hyp_typ
@@ -597,12 +598,6 @@ let elimination_clause_scheme with_evars allow_K elimclause indclause gl =
res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags
gl
-(* cast added otherwise tactics Case (n1,n2) generates (?f x y) and
- * refine fails *)
-
-let type_clenv_binding wc (c,t) lbind =
- clenv_type (make_clenv_binding wc (c,t) lbind)
-
(*
* Elimination tactic with bindings and using an arbitrary
* elimination constant called elimc. This constant should end
@@ -947,7 +942,8 @@ let specialize mopt (c,lbind) g =
else
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 clause = clenv_expand_metas clause in
+ let (thd,tstack) = whd_stack (clenv_direct_value clause) in
let nargs = List.length tstack in
let tstack = match mopt with
| Some m ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 1ebaec3b4..99f2140dd 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -38,9 +38,6 @@ val inj_ebindings : constr bindings -> open_constr bindings
(*s General functions. *)
-val type_clenv_binding : goal sigma ->
- constr * constr -> open_constr bindings -> constr
-
val string_of_inductive : constr -> string
val head_constr : constr -> constr list
val head_constr_bound : constr -> constr list -> constr list
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:30:00 +0000