diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 19 | ||||
| -rw-r--r-- | tactics/equality.mli | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 40 |
3 files changed, 49 insertions, 13 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index cc7701ad5f..18a1f02011 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -736,7 +736,7 @@ let _ = optread = (fun () -> !keep_proof_equalities_for_injection) ; optwrite = (fun b -> keep_proof_equalities_for_injection := b) } -let find_positions env sigma t1 t2 = +let find_positions env sigma ~no_discr t1 t2 = let project env sorts posn t1 t2 = let ty1 = get_type_of env sigma t1 in let s = get_sort_family_of env sigma ty1 in @@ -767,7 +767,7 @@ let find_positions env sigma t1 t2 = List.flatten (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn)) 0 rargs1 rargs2) - else if Sorts.List.mem InType sorts' + else if Sorts.List.mem InType sorts' && not no_discr then (* see build_discriminator *) raise (DiscrFound (List.rev posn,sp1,sp2)) else @@ -791,13 +791,14 @@ let find_positions env sigma t1 t2 = Inl (path,c1,c2) let discriminable env sigma t1 t2 = - match find_positions env sigma t1 t2 with + match find_positions env sigma ~no_discr:false t1 t2 with | Inl _ -> true | _ -> false let injectable env sigma t1 t2 = - match find_positions env sigma t1 t2 with - | Inl _ | Inr [] | Inr [([],_,_)] -> false + match find_positions env sigma ~no_discr:true t1 t2 with + | Inl _ -> assert false + | Inr [] | Inr [([],_,_)] -> false | Inr _ -> true @@ -1032,7 +1033,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - match find_positions env sigma t1 t2 with + match find_positions env sigma ~no_discr:false t1 t2 with | Inr _ -> tclZEROMSG (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> @@ -1414,9 +1415,9 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = let sigma = eq_clause.evd in let env = eq_clause.env in - match find_positions env sigma t1 t2 with + match find_positions env sigma ~no_discr:true t1 t2 with | Inl _ -> - tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.") + assert false | Inr [] -> let suggestion = if !keep_proof_equalities_for_injection then @@ -1483,7 +1484,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause = Proofview.Goal.enter { enter = begin fun gl -> let sigma = clause.evd in let env = Proofview.Goal.env gl in - match find_positions env sigma t1 t2 with + match find_positions env sigma ~no_discr:false t1 t2 with | Inl (cpath, (_,dirn), _) -> discr_positions env sigma u clause cpath dirn | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) diff --git a/tactics/equality.mli b/tactics/equality.mli index d979c580aa..b47be3bbc0 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -96,7 +96,10 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic val rewriteInConcl : bool -> constr -> unit Proofview.tactic +(* Tells if tactic "discriminate" is applicable *) val discriminable : env -> evar_map -> constr -> constr -> bool + +(* Tells if tactic "injection" is applicable *) val injectable : env -> evar_map -> constr -> constr -> bool (* Subst *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 556df6e559..15cef676e6 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2395,6 +2395,29 @@ let rec explicit_intro_names = function explicit_intro_names l | [] -> [] +let rec check_name_unicity env ok seen = function +| (_, IntroForthcoming _) :: l -> check_name_unicity env ok seen l +| (loc, IntroNaming (IntroIdentifier id)) :: l -> + (try + ignore (if List.mem_f Id.equal id ok then raise Not_found else lookup_named id env); + user_err ~loc (pr_id id ++ str" is already used.") + with Not_found -> + if List.mem_f Id.equal id seen then + user_err ~loc (pr_id id ++ str" is used twice.") + else + check_name_unicity env ok (id::seen) l) +| (_, IntroAction (IntroOrAndPattern l)) :: l' -> + let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in + List.iter (fun l -> check_name_unicity env ok seen (l@l')) ll +| (_, IntroAction (IntroInjection l)) :: l' -> + check_name_unicity env ok seen (l@l') +| (_, IntroAction (IntroApplyOn (c,pat))) :: l' -> + check_name_unicity env ok seen (pat::l') +| (_, (IntroNaming (IntroAnonymous | IntroFresh _) + | IntroAction (IntroWildcard | IntroRewrite _))) :: l -> + check_name_unicity env ok seen l +| [] -> () + let wild_id = Id.of_string "_tmp" let rec list_mem_assoc_right id = function @@ -2530,13 +2553,21 @@ and prepare_intros_loc loc with_evars dft destopt = function | IntroForthcoming _ -> user_err ~loc (str "Introduction pattern for one hypothesis expected.") +let intro_patterns_head_core with_evars b destopt bound pat = + Proofview.Goal.enter { enter = begin fun gl -> + let env = Proofview.Goal.env gl in + check_name_unicity env [] [] pat; + intro_patterns_core with_evars b [] [] [] destopt + bound 0 (fun _ l -> clear_wildcards l) pat + end } + let intro_patterns_bound_to with_evars n destopt = - intro_patterns_core with_evars true [] [] [] destopt - (Some (true,n)) 0 (fun _ l -> clear_wildcards l) + intro_patterns_head_core with_evars true destopt + (Some (true,n)) let intro_patterns_to with_evars destopt = - intro_patterns_core with_evars (use_bracketing_last_or_and_intro_pattern ()) - [] [] [] destopt None 0 (fun _ l -> clear_wildcards l) + intro_patterns_head_core with_evars (use_bracketing_last_or_and_intro_pattern ()) + destopt None let intro_pattern_to with_evars destopt pat = intro_patterns_to with_evars destopt [dloc,pat] @@ -4191,6 +4222,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let f (_,is_not_let,_,_) = is_not_let in Array.map (fun (_,l) -> List.map f l) indsign in let names = compute_induction_names branchletsigns names in + Array.iter (check_name_unicity env toclear []) names; let tac = (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) (Tacticals.New.tclTHENLIST [ |