diff options
| author | Pierre-Marie Pédrot | 2020-06-08 15:17:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-19 16:02:25 +0200 |
| commit | 21b4e41544f03de18d9f5b1bdb93a26b36a97999 (patch) | |
| tree | 85e1848df45b189ad40693ebe2b651eae9ba2c1f /plugins | |
| parent | 2a24a665ca63d82ce2576e75636ab6fdbcad9b36 (diff) | |
Opacify the type of hint metadata.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 3dd5059e5d..e365151079 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -205,7 +205,7 @@ open Hints let extend_with_auto_hints env sigma l seq = let f (seq,sigma) p_a_t = - match repr_hint p_a_t.code with + match FullHint.repr p_a_t with | Res_pf (c,_) | Give_exact (c,_) | Res_pf_THEN_trivial_fail (c,_) -> let (c, _, _) = c in |