diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 19:36:45 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:33:39 +0200 |
| commit | 2826683746569b9d78aa01e319315ab554e1619b (patch) | |
| tree | da0933c7169635d9e35003af4d40b0408e7de96d /tactics | |
| parent | 8a3cd2fe699540f1ae5a56917d0f6b951f81d731 (diff) | |
Fix omitted labels in function calls
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 6 | ||||
| -rw-r--r-- | tactics/hints.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 54e4405d1..c430e776a 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -357,12 +357,12 @@ let shelve_dependencies gls = let hintmap_of sigma hdc secvars concl = match hdc with - | None -> fun db -> Hint_db.map_none secvars db + | None -> fun db -> Hint_db.map_none ~secvars db | Some hdc -> fun db -> if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto sigma secvars hdc concl db - else Hint_db.map_existential sigma secvars hdc concl db + Hint_db.map_eauto sigma ~secvars hdc concl db + else Hint_db.map_existential sigma ~secvars hdc concl db (** Hack to properly solve dependent evars that are typeclasses *) let rec e_trivial_fail_db only_classes db_list local_db secvars = diff --git a/tactics/hints.ml b/tactics/hints.ml index bcc068d3d..240178c9a 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1435,7 +1435,7 @@ let pr_hints_db (name,db,hintlist) = let pr_hint_list_for_head c = let dbs = current_db () in let validate (name, db) = - let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in + let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in (name, db, hints) in let valid_dbs = List.map validate dbs in |