aboutsummaryrefslogtreecommitdiff
path: root/vernac/comAssumption.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comAssumption.ml')
-rw-r--r--vernac/comAssumption.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 635751bb24..c37e90650a 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -146,7 +146,7 @@ let do_assumptions ~program_mode kind nl l =
l []
else l
in
- (* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
+ (* We interpret all declarations in the same evar_map, i.e. as a telescope. *)
let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in
let r = Retyping.relevance_of_type env sigma t in