From bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 15:06:26 +0100 Subject: [location] Use located in misctypes. --- proofs/clenv.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs/clenv.ml') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index f9ebc4233..17a9651cd 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -421,7 +421,7 @@ let qhyp_eq h1 h2 = match h1, h2 with | _ -> false let check_bindings bl = - match List.duplicates qhyp_eq (List.map pi2 bl) with + match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with | NamedHyp s :: _ -> user_err (str "The variable " ++ pr_id s ++ @@ -517,7 +517,7 @@ let clenv_match_args bl clenv = let mvs = clenv_independent clenv in check_bindings bl; List.fold_left - (fun clenv (loc,b,c) -> + (fun clenv (loc,(b,c)) -> let k = meta_of_binder clenv loc mvs b in if meta_defined clenv.evd k then if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv @@ -716,7 +716,7 @@ let solve_evar_clause env sigma hyp_only clause = function error_not_right_number_missing_arguments len | ExplicitBindings lbind -> let () = check_bindings lbind in - let fold sigma (_, binder, c) = + let fold sigma (_, (binder, c)) = let ev = evar_of_binder clause.cl_holes binder in define_with_type sigma env ev c in -- cgit v1.2.3