diff options
Diffstat (limited to 'mathcomp/ssreflect/plugin/trunk/ssreflect.ml4')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 40 |
1 files changed, 30 insertions, 10 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index 72161e7..a41da9a 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -4722,19 +4722,35 @@ let rec get_evalref c = match kind_of_term c with | Const (k,_) -> EvalConstRef k | App (c', _) -> get_evalref c' | Cast (c', _, _) -> get_evalref c' - | _ -> errorstrm (str "The term " ++ pr_constr c ++ str " is not unfoldable") + | Proj(c,_) -> EvalConstRef(Projection.constant c) + | _ -> errorstrm (str "The term " ++ pr_constr_pat c ++ str " is not unfoldable") (* Strip a pattern generated by a prenex implicit to its constant. *) -let strip_unfold_term ((sigma, t) as p) kt = match kind_of_term t with +let rec strip_unfold_term env ((sigma, t) as p) kt = match kind_of_term t with | App (f, a) when kt = ' ' && Array.for_all isEvar a && isConst f -> - (sigma, f), true + if Environ.is_projection (fst (destConst f)) env + then strip_unfold_term env (sigma, f) kt + else (sigma, f), true + | Const (c,_) when Environ.is_projection c env -> + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma ((ty,_), sigma, _) = + Evarutil.new_type_evar env sigma (Evd.UnivFlexible true) in + let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma ty in + let sigma = Sigma.to_evar_map sigma in + (sigma, mkProj(Projection.make c false, ev)), true | Const _ | Var _ -> p, true + | Proj _ -> p, true | _ -> p, false +let same_proj t1 t2 = + match kind_of_term t1, kind_of_term t2 with + | Proj(c1,_), Proj(c2, _) -> Projection.equal c1 c2 + | _ -> false + let unfoldintac occ rdx t (kt,_) gl = let fs sigma x = Reductionops.nf_evar sigma x in let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in - let (sigma, t), const = strip_unfold_term t kt in + let (sigma, t), const = strip_unfold_term env0 t kt in let body env t c = Tacred.unfoldn [OnlyOccurrences [1], get_evalref t] env sigma0 c in let easy = occ = None && rdx = None in @@ -4757,14 +4773,17 @@ let unfoldintac occ rdx t (kt,_) gl = | _ -> (fun env (c as orig_c) _ h -> if const then - let rec aux c = - match kind_of_term c with - | Const _ when Term.eq_constr c t -> body env t t - | App (f,a) when Term.eq_constr f t -> mkApp (body env f f,a) - | _ -> let c = Reductionops.whd_betaiotazeta sigma0 c in + let rec aux c = + match kind_of_term c with + | Const _ when Term.eq_constr c t -> body env t t + | App (f,a) when Term.eq_constr f t -> mkApp (body env f f,a) + | Proj _ when same_proj c t -> body env t c + | _ -> + let c = Reductionops.whd_betaiotazeta sigma0 c in match kind_of_term c with | Const _ when Term.eq_constr c t -> body env t t | App (f,a) when Term.eq_constr f t -> mkApp (body env f f,a) + | Proj _ when same_proj c t -> body env t c | Const f -> aux (body env c c) | App (f, a) -> aux (mkApp (body env f f, a)) | _ -> errorstrm (str "The term "++pr_constr orig_c++ @@ -5200,7 +5219,8 @@ ARGUMENT EXTEND ssrunlockargs TYPED AS ssrunlockarg list END let unfoldtac occ ko t kt gl = - let cl, c = pf_fill_occ_term gl occ (fst (strip_unfold_term t kt)) in + let env = pf_env gl in + let cl, c = pf_fill_occ_term gl occ (fst (strip_unfold_term env t kt)) in let cl' = subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref c] gl c) cl in let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in Proofview.V82.of_tactic |