diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 1 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 3 |
2 files changed, 3 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index de49a521fd..4bde427b15 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -603,6 +603,7 @@ let make_hints g st only_classes sign = List.fold_left (fun hints hyp -> let consider = + not only_classes || try let t = hyp |> NamedDecl.get_id |> Global.lookup_named |> NamedDecl.get_type in (* Section variable, reindex only if the type changed *) not (EConstr.eq_constr (project g) (EConstr.of_constr t) (NamedDecl.get_type hyp)) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index aa574e41c5..4101dc23e4 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -468,6 +468,7 @@ module New = struct let check_evars env sigma extsigma origsigma = let rec is_undefined_up_to_restriction sigma evk = + if Evd.mem origsigma evk then None else let evi = Evd.find sigma evk in match Evd.evar_body evi with | Evd.Evar_empty -> Some (evk,evi) @@ -481,7 +482,7 @@ module New = struct let rest = Evd.fold_undefined (fun evk evi acc -> match is_undefined_up_to_restriction sigma evk with - | Some (evk',evi) when not (Evd.mem origsigma evk) -> (evk',evi)::acc + | Some (evk',evi) -> (evk',evi)::acc | _ -> acc) extsigma [] in |