diff options
| author | Pierre-Marie Pédrot | 2020-06-08 12:54:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-19 16:02:25 +0200 |
| commit | f66bd46c551915267a88d1ee2534ba091292882e (patch) | |
| tree | e42293e9c8bdc1fc2aa6888eaddd8c22a2642c0c /tactics/class_tactics.ml | |
| parent | ca6dd2805b4a00cf8425337ec1d89327c94ef397 (diff) | |
Do not export flags in Hints.make_resolves.
They are always the same.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 68a78f52f9..18994d0242 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -524,13 +524,11 @@ let make_resolve_hyp env sigma st only_classes pri decl = (List.map_append (fun (path,info,c) -> let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in - make_resolves env sigma ~name:(PathHints path) - (true, false, false) info ~check:true ~poly:false - h) + make_resolves env sigma ~name:(PathHints path) info ~check:true ~poly:false h) hints) else [] in - (hints @ make_resolves env sigma (true, false, false) pri ~name ~check:false ~poly:false (IsGlobRef id)) + (hints @ make_resolves env sigma pri ~name ~check:false ~poly:false (IsGlobRef id)) else [] let make_hints g (modes,st) only_classes sign = |