From 4865160fa1f2e9ce03b37b9cb3ac99c35e9c4e4d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 20:29:46 +0200
Subject: Renaming interp_rawcontext_evars using a more "standard" name.

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

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4dcf287efc..1d5d8e8658 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2071,7 +2071,7 @@ let intern_context global_level env impl_env binders =
   with InternalizationError (loc,e) ->
     user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
 
-let interp_rawcontext_evars env evdref k bl =
+let interp_glob_context_evars env evdref k bl =
   let open EConstr in
   let (env, par, _, impls) =
     List.fold_left
@@ -2100,6 +2100,6 @@ let interp_rawcontext_evars env evdref k bl =
 
 let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params =
   let int_env,bl = intern_context global_level env impl_env params in
-  let x = interp_rawcontext_evars env evdref shift bl in
+  let x = interp_glob_context_evars env evdref shift bl in
   int_env, x
 
-- 
cgit v1.2.3


From 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 21:41:41 +0200
Subject: Creating a module Nameops.Name extending module Names.Name.

This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.

Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.

Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.
---
 interp/constrintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1d5d8e8658..b8d333f0d0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -536,7 +536,7 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
   try
     (* Binders bound in the notation are considered first-order objects *)
     let _,na = coerce_to_name (fst (Id.Map.find id terms)) in
-    (renaming,{env with ids = name_fold Id.Set.add na env.ids}), na
+    (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -1660,7 +1660,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CCases (sty, rtnpo, tms, eqns) ->
         let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
 	  Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc)
-            (Option.fold_left (fun acc (_,y) -> name_fold Id.Set.add y acc) acc na)
+            (Option.fold_left (fun acc (_,y) -> Name.fold_right Id.Set.add y acc) acc na)
 	    inb) Id.Set.empty tms in
         (* as, in & return vars *)
         let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in
-- 
cgit v1.2.3