diff options
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index b0880065a..9191522dc 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -78,6 +78,7 @@ let pf_interp_type gls c = Astterm.interp_type evc (sig_it gls).evar_env c let pf_global gls id = Declare.construct_reference (sig_it gls).evar_env CCI id + let pf_parse_const gls = compose (pf_global gls) id_of_string let pf_execute gls = |