From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 13 Oct 2015 18:30:47 +0200
Subject: Fix some typos.

---
 pretyping/evarutil.ml | 2 +-
 pretyping/tacred.ml   | 6 +++---
 pretyping/termops.ml  | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8ebb037c24..d3d6901b66 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -525,7 +525,7 @@ let rec check_and_clear_in_constr env evdref err ids c =
 let clear_hyps_in_evi_main env evdref hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
-     the contexts of the evars occuring in evi *)
+     the contexts of the evars occurring in evi *)
   let terms =
     List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in
   let nhyps =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 8a5db90590..48911a5a9f 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1011,8 +1011,8 @@ let contextually byhead occs f env sigma t =
     snd (e_contextually byhead occs f' env sigma t)
 
 (* linear bindings (following pretty-printer) of the value of name in c.
- * n is the number of the next occurence of name.
- * ol is the occurence list to find. *)
+ * n is the number of the next occurrence of name.
+ * ol is the occurrence list to find. *)
 
 let match_constr_evaluable_ref sigma c evref = 
   match kind_of_term c, evref with
@@ -1061,7 +1061,7 @@ let is_projection env = function
 
 (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
- * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
+ * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences.
  * Performs a betaiota reduction after unfolding. *)
 let unfoldoccs env sigma (occs,name) c =
   let unfo nowhere_except_in locs =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 937471cf76..5a55d47fd1 100644
--- a/pretyping/termops.ml
+++ b/pretyping/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 =
-- 
cgit v1.2.3


From 4b8155591be6e20505ee25f7199edcf44a638c7e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Oct 2015 14:38:22 +0200
Subject: Fixing evarmap implementation.

---
 pretyping/evd.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 3d912ca4ce..1107c2951e 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -750,7 +750,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 *)
-- 
cgit v1.2.3


From b8c681338cad546c397a1803c55183cc6526adfb Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 14 Oct 2015 16:39:09 +0200
Subject: Fix constr_matching when a match is found in the head of a case
 construct

---
 pretyping/constr_matching.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 19c85c9e27..121ab74885 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -415,8 +415,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
           try_aux sub mk_ctx next
   | Case (ci,hd,c1,lc) ->
       let next_mk_ctx = function
-      | [] -> assert false
-      | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
+      | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
+      | _ -> assert false
       in
       let sub = (env, c1) :: (env, hd) :: subargs env lc in
       try_aux sub next_mk_ctx next
-- 
cgit v1.2.3


From 26af31cb46c7baf92325dd22bf6ee33aaa2172d2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 14 Oct 2015 18:17:42 +0200
Subject: Occur-check in evar_define was not strong enough.

---
 pretyping/evarsolve.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 754ad8f588..bbc4f1db29 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1484,7 +1484,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
     if occur_meta body then raise MetaOccurInBodyInternal;
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
-    if occur_evar evk body then raise (OccurCheckIn (evd',body));
+    if occur_evar_upto evd' evk body then raise (OccurCheckIn (evd',body));
     (* needed only if an inferred type *)
     let evd', body = refresh_universes pbty env evd' body in
 (* Cannot strictly type instantiations since the unification algorithm
-- 
cgit v1.2.3