diff options
| author | Pierre-Marie Pédrot | 2020-10-29 13:59:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-21 13:55:32 +0100 |
| commit | 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 (patch) | |
| tree | 9913737179ee72e0c1b9672227fe5872ce6734a9 /tactics/auto.ml | |
| parent | a714abe0a1c0cac277297f9e3c7f6d90ac0173d6 (diff) | |
Move evaluable_global_reference from Names to Tacred.
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 369508c2a3..353e138599 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -277,8 +277,8 @@ let hintmap_of env sigma secvars hdc concl = else Hint_db.map_auto env sigma ~secvars hdc concl let exists_evaluable_reference env = function - | EvalConstRef _ -> true - | EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false + | Tacred.EvalConstRef _ -> true + | Tacred.EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false let dbg_intro dbg = tclLOG dbg (fun _ _ -> str "intro") intro let dbg_assumption dbg = tclLOG dbg (fun _ _ -> str "assumption") assumption |