From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- tactics/refine.ml | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) (limited to 'tactics/refine.ml') diff --git a/tactics/refine.ml b/tactics/refine.ml index c1b1fe9d..e7f3998a 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* invalid_arg "Tcc.replace_by_meta (TO DO)" *) in - if occur_meta ty then - error "Unable to manage a dependent metavariable of higher-order type."; mkCast (m,DEFAULTcast, ty),[n,ty],[Some th] exception NoMeta @@ -197,8 +193,6 @@ let rec compute_metamap env sigma c = match kind_of_term c with end | Case (ci,p,cc,v) -> - if occur_meta p then - error "Unable to manage a metavariable in the return clause of a match."; (* bof... *) let nbr = Array.length v in let v = Array.append [|p;cc|] v in @@ -401,5 +395,3 @@ let refine (evd,c) gl = complicated to update meta types when passing through a binder *) let th = compute_metamap (pf_env gl) evd c in tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl - -let _ = Decl_proof_instr.set_refine refine (* dirty trick to solve circular dependency *) -- cgit v1.2.3