diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 09:46:54 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 09:46:54 +0200 |
| commit | 916d5fcc32f5110f23b60b21489d89598e6b8674 (patch) | |
| tree | 2b1d840fa7623d386a0321a380d9f76f03f93841 /tactics/equality.ml | |
| parent | edb55a94fc5c0473e57f5a61c0c723194c2ff414 (diff) | |
| parent | 7952c15ca3d26ae5c2807196bb7aca97bce325c6 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 3e5b7b65f..26e4f01f2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1761,20 +1761,22 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in - let test decl = + let select_equation_name decl = try let lbeq,u,(_,x,y) = find_eq_data_decompose (get_type decl) in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match kind_of_term x, kind_of_term y with - | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z)) -> + | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> + Some (get_id decl) + | _, Var z when not (is_evaluable env (EvalVarRef z)) -> Some (get_id decl) | _ -> None with Constr_matching.PatternMatchingFailure -> None in let hyps = Proofview.Goal.hyps gl in - List.rev (List.map_filter test hyps) + List.rev (List.map_filter select_equation_name hyps) in (* Second step: treat equations *) |