diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-29 09:35:07 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-29 15:29:17 +0200 |
| commit | 4e3d4646788c96f16193df14a81aa79938812194 (patch) | |
| tree | 01494f51829ec148926b7c7d8a8d19dab3cfce51 /tactics/equality.ml | |
| parent | 4e93587fd83bab4ad5c158aa6b3c194e8a7a5551 (diff) | |
Fix a bug in subst releaved by an OCaml warning.
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 06a9b317a..b4c027382 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1730,20 +1730,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 (hyp,_,c) = + let select_equation_name (hyp,_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c 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 hyp + | _, Var z when not (is_evaluable env (EvalVarRef z)) -> Some hyp | _ -> 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 *) |