diff options
Diffstat (limited to 'tactics/refine.ml')
| -rw-r--r-- | tactics/refine.ml | 10 |
1 files changed, 1 insertions, 9 deletions
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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refine.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (* JCF -- 6 janvier 1998 EXPERIMENTAL *) (* @@ -114,8 +112,6 @@ let replace_by_meta env sigma = function | _ -> 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 *) |