aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evd.ml2
-rw-r--r--engine/termops.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 64aad80821..79e73bda57 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -766,7 +766,7 @@ let cmap f evd =
{ evd with
metas = Metamap.map (map_clb f) evd.metas;
defn_evars = EvMap.map (map_evar_info f) evd.defn_evars;
- undf_evars = EvMap.map (map_evar_info f) evd.defn_evars
+ undf_evars = EvMap.map (map_evar_info f) evd.undf_evars
}
(* spiwack: deprecated *)
diff --git a/engine/termops.ml b/engine/termops.ml
index 937471cf76..5a55d47fd1 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -561,7 +561,7 @@ let free_rels m =
in
frec 1 Int.Set.empty m
-(* collects all metavar occurences, in left-to-right order, preserving
+(* collects all metavar occurrences, in left-to-right order, preserving
* repetitions and all. *)
let collect_metas c =