diff options
| author | Gaëtan Gilbert | 2020-03-14 13:09:19 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-14 13:09:19 +0100 |
| commit | 1f984236f4bdc441b80f19bcc32424a45d8168f3 (patch) | |
| tree | 36723e2bfcc13d7cf486404bd0cfdc26781f07bc /tactics/eauto.ml | |
| parent | 5189661a3cc165d8f6cb943c07eb9d644f339102 (diff) | |
| parent | 89d13a553d340ae2a49853597155ab45c0f5a0f4 (diff) | |
Merge PR #10858: Implementing postponed constraints in TC resolution
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index aca6b4734a..9715661985 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -124,7 +124,10 @@ let hintmap_of sigma secvars hdc concl = | None -> fun db -> Hint_db.map_none ~secvars db | Some hdc -> if occur_existential sigma concl then - (fun db -> Hint_db.map_existential sigma ~secvars hdc concl db) + (fun db -> + match Hint_db.map_existential sigma ~secvars hdc concl db with + | ModeMatch l -> l + | ModeMismatch -> []) else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db) (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) |