diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-11 11:55:08 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-17 19:15:20 +0200 |
commit | 94e8664074cfb987f8a63ca29c5436c861184b3a (patch) | |
tree | ed520fdb1120c24fee4285e71ee73448d7d20c56 | |
parent | 6d770156669dd9868ae7623b8f4302866e2cc8c7 (diff) |
Stopping injection not to work on discriminable atoms (see #4890).
-rw-r--r-- | tactics/equality.ml | 19 | ||||
-rw-r--r-- | tactics/equality.mli | 3 |
2 files changed, 13 insertions, 9 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index cc7701ad5..18a1f0201 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 d979c580a..b47be3bbc 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 *) |