diff options
| -rw-r--r-- | pretyping/locusops.ml | 22 | ||||
| -rw-r--r-- | pretyping/locusops.mli | 9 | ||||
| -rw-r--r-- | pretyping/unification.ml | 21 | ||||
| -rw-r--r-- | pretyping/unification.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 48 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 36 |
6 files changed, 81 insertions, 57 deletions
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 21157d9d5a..7e825b6c24 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -87,22 +87,22 @@ let out_arg = function | Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable") | Misctypes.ArgArg x -> x -let occurrences_of_hyp id =function - | LikeFirst -> LikeFirst - | AtOccs cls -> +let occurrences_of_hyp id cls = let rec hyp_occ = function [] -> NoOccurrences, InHyp | ((occs,id'),hl)::_ when Names.Id.equal id id' -> occurrences_map (List.map out_arg) occs, hl | _::l -> hyp_occ l in - AtOccs (match cls.onhyps with + match cls.onhyps with None -> AllOccurrences,InHyp - | Some l -> hyp_occ l) + | Some l -> hyp_occ l -let occurrences_of_goal = function - | LikeFirst -> LikeFirst - | AtOccs cls -> AtOccs (occurrences_map (List.map out_arg) cls.concl_occs) +let occurrences_of_goal cls = + occurrences_map (List.map out_arg) cls.concl_occs -let in_every_hyp = function - | LikeFirst -> true - | AtOccs cls -> Option.is_empty cls.onhyps +let in_every_hyp cls = Option.is_empty cls.onhyps + +let has_selected_occurrences cls = + cls.concl_occs != AllOccurrences || + not (Option.is_empty cls.onhyps) && List.exists (fun ((occs,_),hl) -> + occs != AllOccurrences || hl != InHyp) (Option.get cls.onhyps) diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index f6d27a1850..c1bf2d9eae 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -38,7 +38,8 @@ val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause (** Miscellaneous functions *) -val occurrences_of_hyp : Id.t -> clause or_like_first -> - (occurrences * hyp_location_flag) or_like_first -val occurrences_of_goal : clause or_like_first -> occurrences or_like_first -val in_every_hyp : clause or_like_first -> bool +val occurrences_of_hyp : Id.t -> clause -> (occurrences * hyp_location_flag) +val occurrences_of_goal : clause -> occurrences +val in_every_hyp : clause -> bool + +val has_selected_occurrences : clause -> bool diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 07940bf57d..3f2963bfe5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1468,10 +1468,11 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = else x in + let likefirst = not (has_selected_occurrences occs) in let mkvarid () = mkVar id in let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) = match occurrences_of_hyp hyp occs with - | AtOccs (NoOccurrences, InHyp) -> + | NoOccurrences, InHyp -> if indirectly_dependent c d depdecls then (* Told explicitly not to abstract over [d], but it is dependent *) let id' = indirect_dependency d depdecls in @@ -1480,8 +1481,9 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = ++ str ".") else (push_named_context_val d sign,depdecls) - | (AtOccs (AllOccurrences, InHyp) | LikeFirst) -> - let newdecl = replace_term_occ_decl_modulo LikeFirst test mkvarid d in + | AllOccurrences, InHyp as occ -> + let occ = if likefirst then LikeFirst else AtOccs occ in + let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in if Context.eq_named_declaration d newdecl && not (indirectly_dependent c d depdecls) then @@ -1491,15 +1493,18 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = else (push_named_context_val newdecl sign, newdecl :: depdecls) | occ -> - let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in + (* There are specific occurrences, hence not like first *) + let newdecl = replace_term_occ_decl_modulo (AtOccs occ) test mkvarid d in (push_named_context_val newdecl sign, newdecl :: depdecls) in try let sign,depdecls = fold_named_context compute_dependency env ~init:(empty_named_context_val,[]) in let ccl = match occurrences_of_goal occs with - | AtOccs NoOccurrences -> concl - | occ -> replace_term_occ_modulo occ test mkvarid concl + | NoOccurrences -> concl + | occ -> + let occ = if likefirst then LikeFirst else AtOccs occ in + replace_term_occ_modulo occ test mkvarid concl in let lastlhyp = if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in @@ -1522,7 +1527,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause or_like_first * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool | AbstractExact of Name.t * constr * types option * clause * bool type abstraction_result = @@ -1539,7 +1544,7 @@ let make_abstraction env evd ccl abs = | AbstractExact (name,c,ty,occs,check_occs) -> make_abstraction_core name (make_eq_test env evd c) - env evd c ty (AtOccs occs) check_occs ccl + env evd c ty occs check_occs ccl let keyed_unify env evd kop = if not !keyed_unification then fun cl -> true diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 7f5cac2d23..0f5a62bb5f 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -68,7 +68,7 @@ exception PatternNotFound type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6ce360919c..f315f44455 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2255,7 +2255,7 @@ let letin_pat_tac with_eq id c occs = let sigma = Proofview.Goal.sigma gl in let ccl = Proofview.Goal.concl gl in let check t = true in - let abs = AbstractPattern (false,check,id,c,AtOccs occs,false) in + let abs = AbstractPattern (false,check,id,c,occs,false) in let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in let sigma,c = match res with | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c @@ -3747,34 +3747,24 @@ let induction_without_atomization isrec with_evars elim names lid = (induction_from_context_l with_evars elim_info lid names) end -let has_selected_occurrences = function - | None -> false - | Some cls -> - cls.concl_occs != AllOccurrences || - not (Option.is_empty cls.onhyps) && List.exists (fun ((occs,_),hl) -> - occs != AllOccurrences || hl != InHyp) (Option.get cls.onhyps) - (* assume that no occurrences are selected *) let clear_unselected_context id inhyps cls gl = - match cls with + if occur_var (pf_env gl) id (pf_concl gl) && + cls.concl_occs == NoOccurrences + then errorlabstrm "" + (str "Conclusion must be mentioned: it depends on " ++ pr_id id + ++ str "."); + match cls.onhyps with + | Some hyps -> + let to_erase (id',_,_ as d) = + if Id.List.mem id' inhyps then (* if selected, do not erase *) None + else + (* erase if not selected and dependent on id or selected hyps *) + let test id = occur_var_in_decl (pf_env gl) id d in + if List.exists test (id::inhyps) then Some id' else None in + let ids = List.map_filter to_erase (pf_hyps gl) in + thin ids gl | None -> tclIDTAC gl - | Some cls -> - if occur_var (pf_env gl) id (pf_concl gl) && - cls.concl_occs == NoOccurrences - then errorlabstrm "" - (str "Conclusion must be mentioned: it depends on " ++ pr_id id - ++ str "."); - match cls.onhyps with - | Some hyps -> - let to_erase (id',_,_ as d) = - if Id.List.mem id' inhyps then (* if selected, do not erase *) None - else - (* erase if not selected and dependent on id or selected hyps *) - let test id = occur_var_in_decl (pf_env gl) id d in - if List.exists test (id::inhyps) then Some id' else None in - let ids = List.map_filter to_erase (pf_hyps gl) in - thin ids gl - | None -> tclIDTAC gl let use_bindings env sigma (c,lbind) typ = (* We don't try to normalize the type to an inductive type because *) @@ -3864,9 +3854,8 @@ let pose_induction_arg clear_flag isrec with_evars info_arg elim let ccl = Proofview.Goal.concl gl in Proofview.Refine.refine ~unsafe:true begin fun sigma -> let (sigma',c') = use_bindings env sigma (c0,lbind) t0 in - let occs = match cls with None -> LikeFirst | Some occs -> AtOccs occs in let check = check_enough_applied env sigma elim in - let abs = AbstractPattern (snd info_arg,check,Name id,(pending,c'),occs,false) in + let abs = AbstractPattern (snd info_arg,check,Name id,(pending,c'),cls,false) in let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in match res with | None -> @@ -3895,6 +3884,7 @@ let induction_gen clear_flag isrec with_evars elim Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in + let cls = Option.default allHypsAndConcl cls in let t = typ_of env sigma c in let is_arg_pure_hyp = isVar c && lbind == NoBindings && not with_evars && Option.is_empty eqname @@ -4064,7 +4054,7 @@ let induction_destruct isrec with_evars (lc,elim) = let lc = List.map (on_pi1 (map_induction_arg finish_evar_resolution)) lc in let newlc = List.map (fun (x,(eqn,names),cls) -> - if cls <> None then error "'in' clause not yet supported here."; + if cls != None then error "'in' clause not yet supported here."; match x with (* FIXME: should we deal with ElimOnIdent? *) | _clear_flag,ElimOnConstr x -> if eqn <> None then error "'eqn' clause not supported here."; diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 56ec6a02d6..5f94d8e722 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -256,9 +256,9 @@ Qed. (* Check destruct on idents with maximal implicit arguments - which did not work in 8.4 *) -Parameter f : forall {n:nat}, n=n -> nat. -Goal f (eq_refl 0) = 0. -destruct f. +Parameter g : forall {n:nat}, n=n -> nat. +Goal g (eq_refl 0) = 0. +destruct g. Abort. (* This one was working in 8.4 (because of full conv on closed arguments) *) @@ -278,7 +278,7 @@ Goal forall f : A -> nat -> nat, f a 0 = f a 1. intros. destruct f. -(* This one was not working in 8.4 *) +(* This was not working in 8.4 *) Section S1. Variables x y : Type. @@ -290,6 +290,34 @@ change (x=y) in H. Abort. End S1. +(* This was not working in 8.4 *) + +Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. +intros. +induction g. +2:change (n = g 1 -> n = g 2) in IHn. +Abort. + +(* This was not working in 8.4 *) + +Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. +intros g H H0. +induction g in H |- *. +Abort. + +(* "at" was not granted in 8.4 in the next two examples *) + +Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. +intros g H H0. +induction g in H at 2, H0 at 1. +change (g 0 = 0) in H. +Abort. + +Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. +intros g H H0. +Fail induction g in H at 2 |- *. (* Incompatible occurrences *) +Abort. + (* These ones are not satisfactory at the current time Section S2. |