diff options
| -rw-r--r-- | library/nameops.ml | 2 | ||||
| -rw-r--r-- | library/nameops.mli | 1 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | test-suite/success/dependentind.v | 15 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 9 |
6 files changed, 21 insertions, 15 deletions
diff --git a/library/nameops.ml b/library/nameops.ml index 6c5000dfe..563fa0210 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -143,6 +143,8 @@ let name_fold f na a = | Name id -> f id a | Anonymous -> a +let name_iter f na = name_fold (fun x () -> f x) na () + let name_cons na l = match na with | Anonymous -> l diff --git a/library/nameops.mli b/library/nameops.mli index 336099a2f..10dfecc48 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -34,6 +34,7 @@ val next_name_away_with_default : val out_name : name -> identifier val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a +val name_iter : (identifier -> unit) -> name -> unit val name_cons : name -> identifier list -> identifier list val name_app : (identifier -> identifier) -> name -> name val name_fold_map : ('a -> identifier -> 'a * identifier) -> 'a -> name -> 'a * name diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index ba53d127e..d4b21fba5 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -221,12 +221,15 @@ let rec pat_of_raw metas vars = function PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) | RLambda (_,na,bk,c1,c2) -> + name_iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) - | RProd (_,na,bk,c1,c2) -> + | RProd (_,na,bk,c1,c2) -> + name_iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | RLetIn (_,na,c1,c2) -> + name_iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | RSort (_,s) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index fa0dd6e0c..9940f04b5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2173,8 +2173,8 @@ let abstract_args gl id = let liftargty = lift (List.length ctx) argty in let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in match kind_of_term arg with - | Var _ | Rel _ | Ind _ when convertible -> - (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env) +(* | Var _ | Rel _ | Ind _ when convertible -> *) +(* (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env) *) | _ -> let name = get_id name in let decl = (Name name, None, ty) in diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 3ab7682d9..f0b700adb 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -1,7 +1,6 @@ Require Import Coq.Program.Program. Set Manual Implicit Arguments. - Variable A : Set. Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n). @@ -73,22 +72,20 @@ Proof with simpl in * ; eqns ; eauto with lambda. dependent induction H. - destruct Δ as [|Δ τ']... + destruct Δ as [|Δ τ'']... destruct Δ as [|Δ τ'']... destruct Δ as [|Δ τ'']... apply abs. - - specialize (IHterm (Δ, τ'', τ) Γ0)... + specialize (IHterm (Δ, τ'', τ0) Γ)... intro. eapply app... -Qed. +Defined. Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. Proof with simpl in * ; eqns ; eauto. intros until 1. - dependent induction H. destruct Δ ; eqns. @@ -97,12 +94,12 @@ Proof with simpl in * ; eqns ; eauto. apply ax. destruct Δ... - pose (weakening Γ0 (empty, α))... + pose (weakening Γ (empty, α))... apply weak... apply abs... - specialize (IHterm (Δ, τ))... + specialize (IHterm (Δ, τ0))... eapply app... Defined. @@ -129,5 +126,5 @@ Inductive Ev : forall t, Exp t -> Exp t -> Prop := Ev (Fst e) e1. Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 -> exists e2, Ev e (Pair e1 e2). -intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption. +intros t1 t2 e e1 ev. dependent destruction ev. exists e3 ; assumption. Qed. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index be2f176d3..6c4fe71fc 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -384,6 +384,7 @@ Ltac simplify_one_dep_elim_term c := intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ; case hyp ; clear hyp | block_dep_elim ?T => fail 1 (* Do not put any part of the rhs in the hyps *) + | forall x, _ => intro x || (let H := fresh x in rename x into H ; intro x) (* Try to keep original names *) | _ => intro end. @@ -479,9 +480,11 @@ Ltac intro_prototypes := | _ => idtac end. -Ltac introduce p := - first [ match p with _ => idtac end (* Already there *) - | intros until p | intros ]. +Ltac introduce p := first [ + match p with _ => (* Already there, generalize dependent hyps *) + generalize dependent p ; intros p + end + | intros until p | intros ]. Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)). Ltac do_ind p := introduce p ; (induction p || elim_ind p). |