diff options
| author | Pierre-Marie Pédrot | 2016-08-17 16:17:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-17 16:17:17 +0200 |
| commit | 13fb26d615cdb03a4c4841c20b108deab2de60b3 (patch) | |
| tree | 55f86d47695ee2071d1f886ce70ad7eec6a1e866 /interp | |
| parent | 3fd0b8ad700bd77aabdd3f3f33b13ba5e93d8bc8 (diff) | |
| parent | bc7ffd368789cb82bb8fc8b642b3de870b92c897 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 5 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 2 |
2 files changed, 1 insertions, 6 deletions
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) -> 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,[]) |