Fix ML compilation w.r.t. Coq PR #6536.

herbelin · Jan 30, 2018 · bf1eb50 · bf1eb50
1 parent 7a2d9c4
commit bf1eb50
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/covering.ml b/src/covering.ml
@@ -1327,7 +1327,7 @@ and interp_clause env evars data prev clauses' path (ctx,pats,ctx' as prob) lets
       | Some (clauses, split) -> Some (RecValid (pi1 data, split)))
 
   | By (tac, s) ->
-     let sign, t', rels, _, _ = push_rel_context_to_named_context env' !evars ty in
+     let sign, t', rels, _ = push_rel_context_to_named_context env' !evars ty in
      let sign = named_context_of_val sign in
      let sign', secsign = split_at_eos !evars sign in
      let ids = List.map get_id sign in

diff --git a/src/splitting.ml b/src/splitting.ml
@@ -76,7 +76,7 @@ let map_split f split =
   in aux split
 
 let helper_evar evm evar env typ src =
-  let sign, typ', instance, _, _ = push_rel_context_to_named_context env evm typ in
+  let sign, typ', instance, _ = push_rel_context_to_named_context env evm typ in
   let evm' = evar_declare sign evar typ' ~src evm in
     evm', mkEvar (evar, Array.of_list instance)