From 8d4df809c90352035f7bc92e1f829f2d482625ed Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 10 Aug 2016 11:16:37 +0200
Subject: Make it a bit more obvious when variables are of type unit.

---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 6478ade61a..f3e0682bd7 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1165,7 +1165,7 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
   let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
   (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists)
 
-let rec match_cases_pattern metas (terms,x,termlists,y as sigma) a1 a2 =
+let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
  match (a1,a2) with
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
   | PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
-- 
cgit v1.2.3


From 303f644773969ff84d167e3361c6bb9f9545e8bf Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 16 Aug 2016 20:47:08 +0200
Subject: Removing dead unsafe debugging code in Constrintern.

---
 interp/constrintern.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index fb1baae0a8..7c4688f9fb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -432,11 +432,6 @@ let intern_assumption intern lvar env nal bk ty =
      let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
      env, b
 
-let obj_string x =
-  if Obj.is_block (Obj.repr x) then
-    "tag = " ^ string_of_int (Obj.tag (Obj.repr x))
-  else "int_val = " ^ string_of_int (Obj.magic x)
-
 let rec free_vars_of_pat il =
   function
   | CPatCstr (loc, c, l1, l2) ->
-- 
cgit v1.2.3