aboutsummaryrefslogtreecommitdiff
path: root/pretyping/program.mli
diff options
context:
space:
mode:
authorThéo Zimmermann2019-05-24 16:36:46 +0200
committerThéo Zimmermann2019-05-24 16:36:46 +0200
commit5727443376480be4793757fd5507621ad4f09509 (patch)
tree2fff9e86c24d1d6d82c3ed59919d3b3de4112189 /pretyping/program.mli
parent5596cf352d1c265fd5627dc19416d2b55c10f2b7 (diff)
parentbe40007de49140d403bb1dad1af9f4f1e3fe5003 (diff)
Merge PR #10233: Fixing typos - Part 3
Reviewed-by: Zimmi48
Diffstat (limited to 'pretyping/program.mli')
-rw-r--r--pretyping/program.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/program.mli b/pretyping/program.mli
index a8f5115788..2614e181d6 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -11,7 +11,7 @@
open Names
open EConstr
-(** A bunch of Coq constants used by Progam *)
+(** A bunch of Coq constants used by Program *)
val sig_typ : unit -> GlobRef.t
val sig_intro : unit -> GlobRef.t