aboutsummaryrefslogtreecommitdiff
path: root/pretyping/program.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/program.ml')
-rw-r--r--pretyping/program.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/program.ml b/pretyping/program.ml
index a15e66f329..1bc31646dd 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -11,7 +11,7 @@
open CErrors
open Util
-let papp evdref r args =
+let papp evdref r args =
let open EConstr in
let gr = delayed_force r in
let evd, hd = Evarutil.new_global !evdref gr in