aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/fourier/fourierR.ml2
-rw-r--r--contrib/jprover/jprover.ml42
-rw-r--r--contrib/omega/coq_omega.ml2
-rw-r--r--pretyping/clenv.ml126
-rw-r--r--pretyping/clenv.mli35
-rw-r--r--pretyping/evarutil.ml98
-rw-r--r--pretyping/evarutil.mli30
-rw-r--r--pretyping/evd.ml3
-rw-r--r--pretyping/evd.mli4
-rw-r--r--pretyping/pretyping.mli4
-rw-r--r--pretyping/unification.ml74
-rw-r--r--pretyping/unification.mli12
-rw-r--r--proofs/clenvtac.ml26
-rw-r--r--proofs/clenvtac.mli4
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/evar_tactics.ml6
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/refine.ml4
-rw-r--r--tactics/refine.mli3
-rw-r--r--tactics/setoid_replace.ml10
-rw-r--r--tactics/tactics.ml22
-rw-r--r--tactics/tactics.mli4
24 files changed, 242 insertions, 241 deletions
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 695388130..de7d0b133 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -408,7 +408,7 @@ let tac_zero_infeq_false gl (n,d) =
(tac_zero_inf_pos gl (-n,d)))
;;
-let create_meta () = mkMeta(new_meta());;
+let create_meta () = mkMeta(Evarutil.new_meta());;
let my_cut c gl=
let concl = pf_concl gl in
diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4
index dd76438f6..8de7f37d3 100644
--- a/contrib/jprover/jprover.ml4
+++ b/contrib/jprover/jprover.ml4
@@ -361,7 +361,7 @@ let dyn_impl id gl =
(TCL.tclTHENLAST
(TCL.tclTHENS (T.cut b) [T.intro_using id2;TCL.tclIDTAC])
(T.apply_term (TR.mkVar (short_addr id))
- [TR.mkMeta (Clenv.new_meta())])) gl
+ [TR.mkMeta (Evarutil.new_meta())])) gl
let dyn_allr c = (* [c] must be an eigenvariable which replaces [v] *)
HT.h_intro (N.id_of_string c)
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index ad910b029..86c064098 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -567,7 +567,7 @@ let rec decompile af =
in
loop af.body
-let mkNewMeta () = mkMeta (Clenv.new_meta())
+let mkNewMeta () = mkMeta (Evarutil.new_meta())
let clever_rewrite_base_poly typ p result theorem gl =
let full = pf_concl gl in
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 45ead5a9f..5b4ed6571 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -27,65 +27,47 @@ open Evarutil
open Unification
(* *)
-let w_coerce wc c ctyp target =
+let w_coerce env c ctyp target evd =
let j = make_judge c ctyp in
- let env = Global.env_of_context wc.it in
- let isevars = create_evar_defs wc.sigma in
- let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in
- (evars_of evd',j'.uj_val)
+ let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env evd j target in
+ (evd',j'.uj_val)
let pf_env gls = Global.env_of_context gls.it.evar_hyps
let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c
let pf_hnf_constr gls c = hnf_constr (pf_env gls) gls.sigma c
let pf_concl gl = gl.it.evar_concl
-(* Generator of metavariables *)
-let new_meta =
- let meta_ctr = ref 0 in
- fun () -> incr meta_ctr; !meta_ctr
-
-(* replaces a mapping of existentials into a mapping of metas.
- Problem if an evar appears in the type of another one (pops anomaly) *)
-let exist_to_meta sigma (emap, c) =
- let metamap = ref [] in
- let change_exist evar =
- let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
- let n = new_meta() in
- metamap := (n, ty) :: !metamap;
- mkMeta n in
- let rec replace c =
- match kind_of_term c with
- Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev
- | _ -> map_constr replace c in
- (!metamap, replace c)
-
(******************************************************************)
(* Clausal environments *)
-type wc = named_context sigma
-
type clausenv = {
+ templenv : env;
+ env : evar_defs;
templval : constr freelisted;
templtyp : constr freelisted;
- namenv : identifier Metamap.t;
- env : meta_map;
- hook : wc }
+ namenv : identifier Metamap.t }
+
+let cl_env ce = ce.templenv
+let cl_metas ce = metas_of ce.env
+let cl_sigma ce = evars_of ce.env
-let subst_clenv f sub clenv =
+let subst_clenv sub clenv =
{ templval = map_fl (subst_mps sub) clenv.templval;
templtyp = map_fl (subst_mps sub) clenv.templtyp;
namenv = clenv.namenv;
- env = Metamap.map (map_clb (subst_mps sub)) clenv.env;
- hook = f sub clenv.hook }
+ env = reset_evd
+ (evars_of clenv.env,
+ Metamap.map (map_clb (subst_mps sub)) (cl_metas clenv))
+ clenv.env;
+ templenv = clenv.templenv }
-let clenv_nf_meta clenv c = nf_meta clenv.env c
-let clenv_meta_type clenv mv = meta_type clenv.env mv
-let clenv_value clenv = meta_instance clenv.env clenv.templval
-let clenv_type clenv = meta_instance clenv.env clenv.templtyp
+let clenv_nf_meta clenv c = nf_meta (cl_metas clenv) c
+let clenv_meta_type clenv mv = meta_type (cl_metas clenv) mv
+let clenv_value clenv = meta_instance (cl_metas clenv) clenv.templval
+let clenv_type clenv = meta_instance (cl_metas clenv) clenv.templtyp
-let cl_env ce = Global.env_of_context ce.hook.it
-let clenv_hnf_constr ce t = hnf_constr (cl_env ce) ce.hook.sigma t
+let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
let clenv_get_type_of ce c =
let metamap =
@@ -93,8 +75,8 @@ let clenv_get_type_of ce c =
(function
| (n,Clval(_,typ)) -> (n,typ.rebus)
| (n,Cltyp typ) -> (n,typ.rebus))
- (metamap_to_list ce.env) in
- Retyping.get_type_of_with_meta (cl_env ce) ce.hook.sigma metamap c
+ (metamap_to_list (cl_metas ce)) in
+ Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c
@@ -120,7 +102,7 @@ let clenv_environments bound c =
else
ne
in
- let e' = Metamap.add mv (Cltyp (mk_freelisted c1)) e in
+ let e' = meta_declare mv c1 e in
clrec (ne',e', (mkMeta mv)::metas) (option_app ((+) (-1)) n)
(if dep then (subst1 (mkMeta mv) c2) else c2)
| (n, LetIn (na,b,_,c)) ->
@@ -134,8 +116,8 @@ let mk_clenv_from_n gls n (c,cty) =
{ templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
templtyp = mk_freelisted concl;
namenv = namenv;
- env = env;
- hook = {it=gls.it.evar_hyps; sigma=gls.sigma} }
+ env = mk_evar_defs (gls.sigma,env);
+ templenv = Global.env_of_context gls.it.evar_hyps }
let mk_clenv_from gls = mk_clenv_from_n gls None
@@ -156,7 +138,7 @@ let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
let mentions clenv mv0 =
let rec menrec mv1 =
try
- (match Metamap.find mv1 clenv.env with
+ (match Metamap.find mv1 (cl_metas clenv) with
| Clval (b,_) ->
Metaset.mem mv0 b.freemetas || meta_exists menrec b.freemetas
| Cltyp _ -> false)
@@ -165,7 +147,7 @@ let mentions clenv mv0 =
in
menrec
-let clenv_defined clenv mv = meta_defined clenv.env mv
+let clenv_defined clenv mv = meta_defined (cl_metas clenv) mv
(* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)
let clenv_assign mv rhs clenv =
@@ -173,11 +155,10 @@ let clenv_assign mv rhs clenv =
if meta_exists (mentions clenv mv) rhs_fls.freemetas then
error "clenv__assign: circularity in unification";
try
- (match Metamap.find mv clenv.env with
+ (match Metamap.find mv (cl_metas clenv) with
| Clval (fls,ty) ->
if not (eq_constr fls.rebus rhs) then
try
- (* Streams are lazy, force evaluation of id to catch Not_found*)
let id = Metamap.find mv clenv.namenv in
errorlabstrm "clenv_assign"
(str "An incompatible instantiation has already been found for " ++
@@ -187,19 +168,16 @@ let clenv_assign mv rhs clenv =
else
clenv
| Cltyp bty ->
- { templval = clenv.templval;
- templtyp = clenv.templtyp;
- namenv = clenv.namenv;
- env = Metamap.add mv (Clval (rhs_fls,bty)) clenv.env;
- hook = clenv.hook })
+ { clenv with
+ env = reset_evd
+ (cl_sigma clenv,
+ Metamap.add mv (Clval (rhs_fls,bty)) (cl_metas clenv))
+ clenv.env })
with Not_found ->
error "clenv_assign"
-let clenv_wtactic f clenv =
- let (evd',mmap') =
- f (create_evar_defs clenv.hook.sigma, clenv.env) in
- {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=evars_of evd'}}
+let clenv_wtactic f clenv = {clenv with env = f clenv.env }
(* [clenv_dependent hyps_only clenv]
@@ -225,7 +203,7 @@ let collect_metas c =
* returns a list of the metavars which appear in the type of
* the metavar mv. The list is unordered. *)
-let clenv_metavars clenv mv = (meta_ftype clenv.env mv).freemetas
+let clenv_metavars clenv mv = (meta_ftype (cl_metas clenv) mv).freemetas
let dependent_metas clenv mvs conclmetas =
List.fold_right
@@ -247,8 +225,7 @@ let clenv_missing ce = clenv_dependent true ce
(******************************************************************)
let clenv_unify allow_K cv_pb t1 t2 clenv =
- let env = cl_env clenv in
- clenv_wtactic (w_unify allow_K env cv_pb t1 t2) clenv
+ { clenv with env = w_unify allow_K clenv.templenv cv_pb t1 t2 clenv.env }
let clenv_unique_resolver allow_K clause gl =
clenv_unify allow_K CUMUL (clenv_type clause) (pf_concl gl) clause
@@ -279,8 +256,9 @@ let evar_clenv_unique_resolver clenv gls =
(******************************************************************)
let connect_clenv gls clenv =
- let wc = {it=gls.it.evar_hyps; sigma=gls.sigma} in
- { clenv with hook = wc }
+ { clenv with
+ env = evars_reset_evd gls.sigma clenv.env;
+ templenv = Global.env_of_context gls.it.evar_hyps }
(* [clenv_fchain mv clenv clenv']
*
@@ -308,9 +286,12 @@ let clenv_fchain mv clenv nextclenv =
end else
Metamap.add mv id ne)
clenv.namenv (metamap_to_list nextclenv.namenv);
- env = List.fold_left (fun m (n,v) -> Metamap.add n v m)
- clenv.env (metamap_to_list nextclenv.env);
- hook = nextclenv.hook }
+ env = reset_evd
+ (cl_sigma nextclenv,
+ List.fold_left (fun m (n,v) -> Metamap.add n v m)
+ (cl_metas clenv) (metamap_to_list (cl_metas nextclenv)))
+ nextclenv.env;
+ templenv = nextclenv.templenv }
in
(* unify the type of the template of [nextclenv] with the type of [mv] *)
let clenv'' =
@@ -390,11 +371,11 @@ let clenv_match_args s clause =
with _ ->
(* Try to coerce to the type of [k]; cannot merge with the
previous case because Coercion does not handle Meta *)
- let (_,c') = w_coerce clause.hook c c_typ k_typ in
- try clenv_unify true CONV (mkMeta k) c' clause
- with PretypeError (env,CannotUnify (m,n)) ->
- Stdpp.raise_with_loc loc
- (PretypeError (env,CannotUnifyBindingType (m,n)))
+ let (_,c') = w_coerce (cl_env clause) c c_typ k_typ clause.env in
+ try clenv_unify true CONV (mkMeta k) c' clause
+ with PretypeError (env,CannotUnify (m,n)) ->
+ Stdpp.raise_with_loc loc
+ (PretypeError (env,CannotUnifyBindingType (m,n)))
in matchrec cl t
in
matchrec clause s
@@ -435,14 +416,13 @@ let clenv_constrain_dep_args hyps_only clause = function
if List.length occlist = List.length mlist then
List.fold_left2
(fun clenv k c ->
- let wc = clause.hook in
try
let k_typ =
clenv_hnf_constr clause (clenv_meta_type clause k) in
let c_typ =
clenv_hnf_constr clause (clenv_get_type_of clause c) in
(* faire quelque chose avec le sigma retourne ? *)
- let (_,c') = w_coerce wc c c_typ k_typ in
+ let (_,c') = w_coerce (cl_env clenv) c c_typ k_typ clenv.env in
clenv_unify true CONV (mkMeta k) c' clenv
with _ ->
clenv_unify true CONV (mkMeta k) c clenv)
@@ -494,4 +474,4 @@ let pr_clenv clenv =
in
(str"TEMPL: " ++ print_constr clenv.templval.rebus ++
str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
- (prlist pr_meta_binding (metamap_to_list clenv.env)))
+ (prlist pr_meta_binding (metamap_to_list (cl_metas clenv))))
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 375d84eac..30bc96338 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -13,40 +13,31 @@ open Util
open Names
open Term
open Sign
+open Environ
open Evd
open Evarutil
(*i*)
-(* [new_meta] is a generator of unique meta variables *)
-val new_meta : unit -> metavariable
-
-(* [exist_to_meta] generates new metavariables for each existential
- and performs the replacement in the given constr *)
-val exist_to_meta :
- evar_map -> Pretyping.open_constr -> (Termops.metamap * constr)
-
(***************************************************************)
(* The Type of Constructions clausale environments. *)
-(* [templval] is the template which we are trying to fill out.
+(* [templenv] is the typing context
+ * [env] is the mapping from metavar and evar numbers to their types
+ * and values.
+ * [templval] is the template which we are trying to fill out.
* [templtyp] is its type.
* [namenv] is a mapping from metavar numbers to names, for
* use in instanciating metavars by name.
- * [evd] is the mapping from metavar and evar numbers to their types
- * and values.
- * [hook] is a signature (named_context) and a sigma: the
- * typing context
*)
-type wc = named_context sigma (* for a better reading of the following *)
type clausenv = {
+ templenv : env;
+ env : evar_defs;
templval : constr freelisted;
templtyp : constr freelisted;
- namenv : identifier Metamap.t;
- env : meta_map;
- hook : wc }
+ namenv : identifier Metamap.t }
-val subst_clenv :
- (substitution -> wc -> wc) -> substitution -> clausenv -> clausenv
+(* Substitution is not applied neither to the evar_map of evar_defs nor hook *)
+val subst_clenv : substitution -> clausenv -> clausenv
(* subject of clenv (instantiated) *)
val clenv_value : clausenv -> constr
@@ -118,9 +109,3 @@ val make_clenv_binding :
(* Pretty-print *)
val pr_clenv : clausenv -> Pp.std_ppcmds
-(***************************************************************)
-(* Old or unused stuff... *)
-
-val clenv_wtactic :
- (evar_defs * meta_map -> evar_defs * meta_map) -> clausenv -> clausenv
-
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 9a4c9cfed..cb4efd2e1 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -92,6 +92,63 @@ let nf_evar_info evc info =
evar_body = info.evar_body}
(**********************)
+(* Creating new metas *)
+(**********************)
+
+(* Generator of metavariables *)
+let new_meta =
+ let meta_ctr = ref 0 in
+ fun () -> incr meta_ctr; !meta_ctr
+
+let mk_new_meta () = mkMeta(new_meta())
+
+(* replaces a mapping of existentials into a mapping of metas.
+ Problem if an evar appears in the type of another one (pops anomaly) *)
+let exist_to_meta sigma (emap, c) =
+ let metamap = ref [] in
+ let change_exist evar =
+ let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
+ let n = new_meta() in
+ metamap := (n, ty) :: !metamap;
+ mkMeta n in
+ let rec replace c =
+ match kind_of_term c with
+ Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev
+ | _ -> map_constr replace c in
+ (!metamap, replace c)
+
+(*************************************)
+(* Metas *)
+
+let meta_val_of env mv =
+ let rec valrec mv =
+ try
+ (match Metamap.find mv env with
+ | Cltyp _ -> mkMeta mv
+ | Clval(b,_) ->
+ instance (List.map (fun mv' -> (mv',valrec mv'))
+ (Metaset.elements b.freemetas)) b.rebus)
+ with Not_found ->
+ mkMeta mv
+ in
+ valrec mv
+
+let meta_instance env b =
+ let c_sigma =
+ List.map
+ (fun mv -> (mv,meta_val_of env mv)) (Metaset.elements b.freemetas)
+ in
+ instance c_sigma b.rebus
+
+let nf_meta env c = meta_instance env (mk_freelisted c)
+
+let meta_type env mv =
+ let ty =
+ try meta_ftype env mv
+ with Not_found -> error ("unknown meta ?"^string_of_int mv) in
+ meta_instance env ty
+
+(**********************)
(* Creating new evars *)
(**********************)
@@ -216,15 +273,22 @@ let do_restrict_hyps sigma ev args =
* operations on the evar constraints *
*------------------------------------*)
+type maps = evar_map * meta_map
type evar_constraint = conv_pb * constr * constr
type evar_defs =
{ evars : Evd.evar_map;
conv_pbs : evar_constraint list;
- history : (existential_key * (loc * Rawterm.hole_kind)) list }
+ history : (existential_key * (loc * Rawterm.hole_kind)) list;
+ metas : Evd.meta_map }
-let create_evar_defs evd = { evars=evd; conv_pbs=[]; history=[] }
+let mk_evar_defs (sigma,mmap) =
+ { evars=sigma; conv_pbs=[]; history=[]; metas=mmap }
+let create_evar_defs sigma =
+ mk_evar_defs (sigma,Metamap.empty)
let evars_of d = d.evars
+let metas_of d = d.metas
let evars_reset_evd evd d = {d with evars = evd}
+let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap}
let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
let evar_source ev d =
try List.assoc ev d.history
@@ -594,33 +658,3 @@ let valcon_of_tycon x = x
let lift_tycon = option_app (lift 1)
-(*************************************)
-(* Metas *)
-
-let meta_val_of env mv =
- let rec valrec mv =
- try
- (match Metamap.find mv env with
- | Cltyp _ -> mkMeta mv
- | Clval(b,_) ->
- instance (List.map (fun mv' -> (mv',valrec mv'))
- (Metaset.elements b.freemetas)) b.rebus)
- with Not_found ->
- mkMeta mv
- in
- valrec mv
-
-let meta_instance env b =
- let c_sigma =
- List.map
- (fun mv -> (mv,meta_val_of env mv)) (Metaset.elements b.freemetas)
- in
- instance c_sigma b.rebus
-
-let nf_meta env c = meta_instance env (mk_freelisted c)
-
-let meta_type env mv =
- let ty =
- try meta_ftype env mv
- with Not_found -> error ("unknown meta ?"^string_of_int mv) in
- meta_instance env ty
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 4223b0e78..6d264b718 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -40,19 +40,40 @@ exception Uninstantiated_evar of existential_key
val whd_ise : evar_map -> constr -> constr
val whd_castappevar : evar_map -> constr -> constr
+(***********************************************************)
+(* Metas *)
+
+(* [new_meta] is a generator of unique meta variables *)
+val new_meta : unit -> metavariable
+val mk_new_meta : unit -> constr
+val nf_meta : meta_map -> constr -> constr
+val meta_type : meta_map -> metavariable -> types
+val meta_instance : meta_map -> constr freelisted -> constr
+
+(* [exist_to_meta] generates new metavariables for each existential
+ and performs the replacement in the given constr *)
+val exist_to_meta : evar_map -> open_constr -> (Termops.metamap * constr)
+
(* Creating new existential variables *)
val new_evar : unit -> evar
val new_evar_in_sign : env -> constr
val evar_env : evar_info -> env
+(***********************************************************)
+
+type maps = evar_map * meta_map
type evar_defs
-val evars_of : evar_defs -> evar_map
+val evars_of : evar_defs -> evar_map
+val metas_of : evar_defs -> meta_map
val non_instantiated : evar_map -> (evar * evar_info) list
-val create_evar_defs : evar_map -> evar_defs
+val mk_evar_defs : maps -> evar_defs
+(* the same with empty meta map: *)
+val create_evar_defs : evar_map -> evar_defs
val evars_reset_evd : evar_map -> evar_defs -> evar_defs
+val reset_evd : maps -> evar_defs -> evar_defs
val evar_source : existential_key -> evar_defs -> loc * hole_kind
type evar_constraint = conv_pb * constr * constr
@@ -82,6 +103,7 @@ val solve_simple_eqn :
val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types
val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
+(***********************************************************)
(* Value/Type constraints *)
val new_Type_sort : unit -> sorts
@@ -105,7 +127,3 @@ val valcon_of_tycon : type_constraint -> val_constraint
val lift_tycon : type_constraint -> type_constraint
-(* Metas *)
-val nf_meta : meta_map -> constr -> constr
-val meta_type : meta_map -> metavariable -> types
-val meta_instance : meta_map -> constr freelisted -> constr
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index be35cb947..d7468eded 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -118,6 +118,9 @@ let existential_opt_value sigma ev =
with NotInstantiatedEvar -> None
(*******************************************************************)
+type open_constr = evar_map * constr
+
+(*******************************************************************)
(* The type constructor ['a sigma] adds an evar map to an object of
type ['a] *)
type 'a sigma = {
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 3f9eaa5fa..df362a9bf 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -64,6 +64,10 @@ val existential_type : evar_map -> existential -> types
val existential_opt_value : evar_map -> existential -> constr option
(*************************)
+(* constr with holes *)
+type open_constr = evar_map * constr
+
+(*************************)
(* The type constructor ['a sigma] adds an evar map to an object of
type ['a] *)
type 'a sigma = {
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 57a3d1be8..096c982c5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -20,10 +20,6 @@ open Evarutil
type var_map = (identifier * unsafe_judgment) list
-(* constr with holes *)
-type open_constr = evar_map * constr
-
-
(* Generic call to the interpreter from rawconstr to constr, failing
unresolved holes in the rawterm cannot be instantiated.
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4a9cab206..33f09fd0a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -49,14 +49,12 @@ let abstract_list_all env sigma typ c l =
(*******************************)
-type maps = evar_defs * meta_map
-
-let w_Declare env sp ty (evd,mmap) =
+let w_Declare env sp ty evd =
let sigma = evars_of evd in
let _ = Typing.type_of env sigma ty in (* Utile ?? *)
let newdecl =
{ evar_hyps=named_context env; evar_concl=ty; evar_body=Evar_empty } in
- (evars_reset_evd (Evd.add sigma sp newdecl) evd, mmap)
+ evars_reset_evd (Evd.add sigma sp newdecl) evd
(* [w_Define evd sp c]
*
@@ -66,7 +64,7 @@ let w_Declare env sp ty (evd,mmap) =
* No unification is performed in order to assert that [c] has the
* correct type.
*)
-let w_Define sp c (evd,mmap) =
+let w_Define sp c evd =
let sigma = evars_of evd in
if Evd.is_defined sigma sp then
error "Unify.w_Define: cannot define evar twice";
@@ -82,7 +80,7 @@ let w_Define sp c (evd,mmap) =
(str "Cannot use variable " ++ pr_id v ++ str " to define " ++
str (string_of_existential sp)) in
let spdecl' = { spdecl with evar_body = Evar_defined c } in
- (evars_reset_evd (Evd.add sigma sp spdecl') evd, mmap)
+ evars_reset_evd (Evd.add sigma sp spdecl') evd
(* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
@@ -230,17 +228,17 @@ let is_mimick_head f =
or in evars, possibly generating new unification problems; if [b]
is true, unification of types of metas is required *)
-let w_merge env with_types metas evars maps =
+let w_merge env with_types metas evars evd =
let ty_metas = ref [] in
let ty_evars = ref [] in
- let rec w_merge_rec (evd,mmap as maps) metas evars =
+ let rec w_merge_rec evd metas evars =
match (evars,metas) with
- | ([], []) -> maps
+ | ([], []) -> evd
| ((lhs,rhs)::t, metas) ->
(match kind_of_term rhs with
- | Meta k -> w_merge_rec maps ((k,lhs)::metas) t
+ | Meta k -> w_merge_rec evd ((k,lhs)::metas) t
| krhs ->
(match kind_of_term lhs with
@@ -249,7 +247,7 @@ let w_merge env with_types metas evars maps =
if is_defined_evar evd ev then
let (metas',evars') =
unify_0 env (evars_of evd) CONV rhs lhs in
- w_merge_rec maps (metas'@metas) (evars'@t)
+ w_merge_rec evd (metas'@metas) (evars'@t)
else begin
let rhs' =
if occur_meta rhs then subst_meta metas rhs else rhs
@@ -259,23 +257,24 @@ let w_merge env with_types metas evars maps =
match krhs with
| App (f,cl) when is_mimick_head f ->
(try
- w_merge_rec (w_Define evn rhs' maps) metas t
+ w_merge_rec (w_Define evn rhs' evd) metas t
with ex when precatchable_exception ex ->
- let maps' =
- mimick_evar maps f (Array.length cl) evn in
- w_merge_rec maps' metas evars)
+ let evd' =
+ mimick_evar evd f (Array.length cl) evn in
+ w_merge_rec evd' metas evars)
| _ ->
(* ensure tail recursion in non-mimickable case! *)
- w_merge_rec (w_Define evn rhs' maps) metas t
+ w_merge_rec (w_Define evn rhs' evd) metas t
end
| _ -> anomaly "w_merge_rec"))
| ([], (mv,n)::t) ->
+ let mmap = metas_of evd in
if meta_defined mmap mv then
let (metas',evars') =
unify_0 env (evars_of evd) CONV (meta_fvalue mmap mv).rebus n in
- w_merge_rec maps (metas'@t) evars'
+ w_merge_rec evd (metas'@t) evars'
else
begin
if with_types (* or occur_meta mvty *) then
@@ -288,30 +287,31 @@ let w_merge env with_types metas evars maps =
ty_metas := mc @ !ty_metas;
ty_evars := ec @ !ty_evars
with e when precatchable_exception e -> ());
- let mmap' = meta_assign mv n mmap in
- w_merge_rec (evd,mmap') t []
+ let evd' =
+ reset_evd (evars_of evd,meta_assign mv n mmap) evd in
+ w_merge_rec evd' t []
end
- and mimick_evar (evd,mmap) hdc nargs sp =
+ and mimick_evar evd hdc nargs sp =
let ev = Evd.map (evars_of evd) sp in
let sp_env = Global.env_of_context ev.evar_hyps in
let (evd', c) = applyHead sp_env evd nargs hdc in
let (mc,ec) =
unify_0 sp_env (evars_of evd') CUMUL
(Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in
- let maps' = w_merge_rec (evd',mmap) mc ec in
- if (evars_of evd') == (evars_of (fst maps'))
- then w_Define sp c maps'
- else w_Define sp (Evarutil.nf_evar (evars_of (fst maps')) c) maps' in
+ let evd'' = w_merge_rec evd' mc ec in
+ if (evars_of evd') == (evars_of evd'')
+ then w_Define sp c evd''
+ else w_Define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in
(* merge constraints *)
- let maps' = w_merge_rec maps metas evars in
+ let evd' = w_merge_rec evd metas evars in
if with_types then
(* merge constraints about types: if they fail, don't worry *)
- try w_merge_rec maps' !ty_metas !ty_evars
- with e when precatchable_exception e -> maps'
+ try w_merge_rec evd' !ty_metas !ty_evars
+ with e when precatchable_exception e -> evd'
else
- maps'
+ evd'
(* [w_unify env evd M N]
performs a unification of M and N, generating a bunch of
@@ -324,7 +324,7 @@ let w_merge env with_types metas evars maps =
types of metavars are unifiable with the types of their instances *)
let w_unify_core_0 env with_types cv_pb m n evd =
- let (mc,ec) = unify_0 env (evars_of (fst evd)) cv_pb m n in
+ let (mc,ec) = unify_0 env (evars_of evd) cv_pb m n in
w_merge env with_types mc ec evd
let w_unify_0 env = w_unify_core_0 env false
@@ -418,19 +418,19 @@ let w_unify_to_subterm_list env allow_K oplist t evd =
with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op)
in
(evd',cl::l)
- else if not allow_K & not (dependent op t) then
- (* This is not up to delta ... *)
- raise (PretypeError (env,NoOccurrenceFound op))
+ else if allow_K or dependent op t then
+ (evd,op::l)
else
- (evd,op::l))
+ (* This is not up to delta ... *)
+ raise (PretypeError (env,NoOccurrenceFound op)))
oplist
(evd,[])
let secondOrderAbstraction env allow_K typ (p, oplist) evd =
- let sigma = evars_of (fst evd) in
+ let sigma = evars_of evd in
let (evd',cllist) =
w_unify_to_subterm_list env allow_K oplist typ evd in
- let typp = meta_type (snd evd') p in
+ let typp = meta_type (metas_of evd') p in
let pred = abstract_list_all env sigma typp typ cllist in
w_unify_0 env CONV (mkMeta p) pred evd'
@@ -443,13 +443,13 @@ let w_unify2 env allow_K cv_pb ty1 ty2 evd =
let evd' =
secondOrderAbstraction env allow_K ty2 (p1,oplist1) evd in
(* Resume first order unification *)
- w_unify_0 env cv_pb (nf_meta (snd evd') ty1) ty2 evd'
+ w_unify_0 env cv_pb (nf_meta (metas_of evd') ty1) ty2 evd'
| _, Meta p2 ->
(* Find the predicate *)
let evd' =
secondOrderAbstraction env allow_K ty1 (p2, oplist2) evd in
(* Resume first order unification *)
- w_unify_0 env cv_pb ty1 (nf_meta (snd evd') ty2) evd'
+ w_unify_0 env cv_pb ty1 (nf_meta (metas_of evd') ty2) evd'
| _ -> error "w_unify2"
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 02d1918be..d3007e69d 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -18,19 +18,19 @@ open Evd
open Evarutil
(*i*)
-type maps = evar_defs * meta_map
-
-val w_Declare : env -> evar -> types -> maps -> maps
-val w_Define : evar -> constr -> maps -> maps
+val w_Declare : env -> evar -> types -> evar_defs -> evar_defs
+val w_Define : evar -> constr -> evar_defs -> evar_defs
(* The "unique" unification fonction *)
val w_unify :
- bool -> env -> Reductionops.conv_pb -> constr -> constr -> maps -> maps
+ bool -> env -> Reductionops.conv_pb -> constr -> constr ->
+ evar_defs -> evar_defs
(* [w_unify_to_subterm env (c,t) m] performs unification of [c] with a
subterm of [t]. Constraints are added to [m] and the matched
subterm of [t] is also returned. *)
-val w_unify_to_subterm : env -> constr * constr -> maps -> maps * constr
+val w_unify_to_subterm :
+ env -> constr * constr -> evar_defs -> evar_defs * constr
(*i This should be in another module i*)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 2d972068d..aa2ff18ce 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -48,7 +48,7 @@ let clenv_cast_meta clenv =
match kind_of_term (strip_outer_cast u) with
| Meta mv ->
(try
- match Metamap.find mv clenv.env with
+ match Metamap.find mv (metas_of clenv.env) with
| Cltyp b ->
let b' = clenv_nf_meta clenv b.rebus in
if occur_meta b' then u else mkCast (mkMeta mv, b')
@@ -62,26 +62,14 @@ let clenv_cast_meta clenv =
in
crec
-
let clenv_refine clenv gls =
tclTHEN
- (tclEVARS clenv.hook.sigma)
- (refine (clenv_value clenv)) gls
-
-let clenv_refine_cast clenv gls =
- tclTHEN
- (tclEVARS clenv.hook.sigma)
+ (tclEVARS (evars_of clenv.env))
(refine (clenv_cast_meta clenv (clenv_value clenv)))
gls
-let res_pf clenv gls =
- clenv_refine (clenv_unique_resolver false clenv gls) gls
-
-let res_pf_cast clenv gls =
- clenv_refine_cast (clenv_unique_resolver false clenv gls) gls
-
-let elim_res_pf clenv allow_K gls =
- clenv_refine_cast (clenv_unique_resolver allow_K clenv gls) gls
+let res_pf clenv ?(allow_K=false) gls =
+ clenv_refine (clenv_unique_resolver allow_K clenv gls) gls
let elim_res_pf_THEN_i clenv tac gls =
let clenv' = (clenv_unique_resolver true clenv gls) in
@@ -102,9 +90,9 @@ let e_res_pf clenv gls =
(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
let unifyTerms m n gls =
let env = pf_env gls in
- let maps = (create_evar_defs (project gls), Evd.Metamap.empty) in
- let maps' = Unification.w_unify false env CONV m n maps in
- tclIDTAC {it = gls.it; sigma = evars_of (fst maps')}
+ let evd = create_evar_defs (project gls) in
+ let evd' = Unification.w_unify false env CONV m n evd in
+ tclIDTAC {it = gls.it; sigma = evars_of evd'}
let unify m gls =
let n = pf_concl gls in unifyTerms m n gls
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index c463d75e3..cc75af0fc 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -21,8 +21,6 @@ open Proof_type
(* Tactics *)
val unify : constr -> tactic
val clenv_refine : clausenv -> tactic
-val res_pf : clausenv -> tactic
-val res_pf_cast : clausenv -> tactic
-val elim_res_pf : clausenv -> bool -> tactic
+val res_pf : clausenv -> ?allow_K:bool -> tactic
val e_res_pf : clausenv -> tactic
val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 66454059e..c32130d2c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -323,7 +323,7 @@ let forward_subst_tactic =
let set_extern_subst_tactic f = forward_subst_tactic := f
let subst_autohint (_,subst,(local,name,hintlist as obj)) =
- let trans_clenv clenv = Clenv.subst_clenv (fun _ a -> a) subst clenv in
+ let trans_clenv clenv = Clenv.subst_clenv subst clenv in
let trans_data data code =
{ data with
pat = option_smartmap (subst_pattern subst) data.pat ;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 38dc8f58e..f9834f522 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -821,7 +821,7 @@ let swap_equands gls eqn =
let swapEquandsInConcl gls =
let (lbeq,(t,e1,e2)) = find_eq_data_decompose (pf_concl gls) in
let sym_equal = lbeq.sym in
- refine (applist(sym_equal,[t;e2;e1;mkMeta (Clenv.new_meta())])) gls
+ refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls
let swapEquandsInHyp id gls =
((tclTHENS (cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id)))
@@ -880,8 +880,8 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
else
(build_non_dependent_rewrite_predicate (t,e1,e2) body gls)
in
- refine (applist(eq_elim,[t;e1;p;mkMeta(Clenv.new_meta());
- e2;mkMeta(Clenv.new_meta())])) gls
+ refine (applist(eq_elim,[t;e1;p;Evarutil.mk_new_meta();
+ e2;Evarutil.mk_new_meta()])) gls
(* [subst_tuple_term dep_pair B]
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index b5a0370c7..f2db79d1a 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -67,7 +67,7 @@ let instantiate_tac = function
let let_evar nam typ gls =
let sp = Evarutil.new_evar () in
- let mm = (Evarutil.create_evar_defs gls.sigma, Metamap.empty) in
- let (evd,_) = Unification.w_Declare (pf_env gls) sp typ mm in
- let ngls = {gls with sigma = Evarutil.evars_of evd} in
+ let evd = Evarutil.create_evar_defs gls.sigma in
+ let evd' = Unification.w_Declare (pf_env gls) sp typ evd in
+ let ngls = {gls with sigma = Evarutil.evars_of evd'} in
Tactics.forward true nam (mkEvar(sp,[||])) ngls
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 0ac120327..1e4267421 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -475,7 +475,7 @@ let raw_inversion inv_kind indbinding id status names gl =
(fun id ->
(tclTHEN
(apply_term (mkVar id)
- (list_tabulate (fun _ -> mkMeta(Clenv.new_meta())) neqns))
+ (list_tabulate (fun _ -> Evarutil.mk_new_meta()) neqns))
reflexivity))])
gl
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index aa980fd47..9fd54ee69 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -289,7 +289,7 @@ let lemInv id c gls =
try
let clause = mk_clenv_type_of gls c in
let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in
- Clenvtac.elim_res_pf clause true gls
+ Clenvtac.res_pf clause ~allow_K:true gls
with
| UserError (a,b) ->
errorlabstrm "LemInv"
diff --git a/tactics/refine.ml b/tactics/refine.ml
index aa9cf2c57..88e2fcea8 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -92,7 +92,7 @@ and pp_sg sg =
let replace_by_meta env gmm = function
| TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp
| (TH (c,mm,_)) as th ->
- let n = Clenv.new_meta() in
+ let n = Evarutil.new_meta() in
let m = mkMeta n in
(* quand on introduit une mv on calcule son type *)
let ty = match kind_of_term c with
@@ -340,7 +340,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as th) gl =
let refine oc gl =
let sigma = project gl in
let env = pf_env gl in
- let (gmm,c) = Clenv.exist_to_meta sigma oc in
+ let (gmm,c) = Evarutil.exist_to_meta sigma oc in
let th = compute_metamap env gmm c in
tcc_aux [] th gl
diff --git a/tactics/refine.mli b/tactics/refine.mli
index 26cd04ef0..89e531675 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.mli
@@ -8,7 +8,6 @@
(*i $Id$ i*)
-open Term
open Tacmach
-val refine : Pretyping.open_constr -> tactic
+val refine : Evd.open_constr -> tactic
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 905ca60b4..853b4e295 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -22,6 +22,8 @@ open Util
open Pp
open Printer
open Environ
+open Clenv
+open Unification
open Tactics
open Tacticals
open Vernacexpr
@@ -919,7 +921,7 @@ let syntactic_but_representation_of_marked_but hole_relation =
else
let c_is_proper =
let typ = mkApp (rel_out, [| c ; c |]) in
- mkCast (mkMeta (Clenv.new_meta ()),typ)
+ mkCast (Evarutil.mk_new_meta (),typ)
in
mkApp ((Lazy.force coq_ProperElementToKeep),
[| hole_relation ; Lazy.force coq_Left2Right; precise_out ;
@@ -958,9 +960,7 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl =
let but = pf_concl gl in
let (hyp,c1,c2) =
let cl' =
- Clenv.clenv_wtactic
- (fun evd-> fst (Unification.w_unify_to_subterm (pf_env gl) (c1,but) evd))
- cl in
+ {cl with env = fst (w_unify_to_subterm (pf_env gl) (c1,but) cl.env)} in
let c1 = Clenv.clenv_nf_meta cl' c1 in
let c2 = Clenv.clenv_nf_meta cl' c2 in
(lft2rgt,Clenv.clenv_value cl'), c1, c2
@@ -974,7 +974,7 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl =
let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in
let th' = mkApp ((Lazy.force coq_proj2), [|impl1; impl2; th|]) in
Tactics.refine
- (mkApp (th', [| mkCast (mkMeta (Clenv.new_meta()), hyp1) |])) gl
+ (mkApp (th', [| mkCast (Evarutil.mk_new_meta(), hyp1) |])) gl
let general_s_rewrite lft2rgt c gl =
let ctype = pf_type_of gl c in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 57804f23a..e6b2f76ec 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -40,6 +40,7 @@ open Nametab
open Genarg
open Tacexpr
open Decl_kinds
+open Evarutil
exception Bound
@@ -421,7 +422,7 @@ let rec intros_rmove = function
* of the type of a term. *)
let apply_type hdcty argl gl =
- refine (applist (mkCast (mkMeta (new_meta()),hdcty),argl)) gl
+ refine (applist (mkCast (Evarutil.mk_new_meta(),hdcty),argl)) gl
let apply_term hdc argl gl =
refine (applist (hdc,argl)) gl
@@ -431,17 +432,12 @@ let bring_hyps hyps =
else
(fun gl ->
let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in
- let f = mkCast (mkMeta (new_meta()),newcl) in
+ let f = mkCast (Evarutil.mk_new_meta(),newcl) in
refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
(* Resolution with missing arguments *)
let apply_with_bindings (c,lbind) gl =
- let apply =
- match kind_of_term c with
- | Lambda _ -> Clenvtac.res_pf_cast
- | _ -> Clenvtac.res_pf
- in
(* The actual type of the theorem. It will be matched against the
goal. If this fails, then the head constant will be unfolded step by
step. *)
@@ -451,7 +447,7 @@ let apply_with_bindings (c,lbind) gl =
let n = nb_prod thm_ty - nb_prod (pf_concl gl) in
if n<0 then error "Apply: theorem has not enough premisses.";
let clause = make_clenv_binding_apply gl n (c,thm_ty) lbind in
- apply clause gl
+ Clenvtac.res_pf clause gl
with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn ->
let red_thm =
try red_product (pf_env gl) (project gl) thm_ty
@@ -462,7 +458,7 @@ let apply_with_bindings (c,lbind) gl =
(* Last chance: if the head is a variable, apply may try
second order unification *)
let clause = make_clenv_binding_apply gl (-1) (c,thm_ty0) lbind in
- apply clause gl
+ Clenvtac.res_pf clause gl
let apply c = apply_with_bindings (c,NoBindings)
@@ -838,7 +834,7 @@ let new_hyp mopt (c,lbind) g =
| Some m -> if m < nargs then list_firstn m tstack else tstack
| None -> tstack)
in
- (tclTHENLAST (tclTHEN (tclEVARS clause.hook.sigma)
+ (tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.env))
(cut (pf_type_of g cut_pf)))
((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
@@ -905,7 +901,7 @@ let elimination_clause_scheme elimclause indclause allow_K gl =
(str "The type of elimination clause is not well-formed"))
in
let elimclause' = clenv_fchain indmv elimclause indclause in
- elim_res_pf elimclause' allow_K gl
+ res_pf elimclause' ~allow_K:allow_K gl
(* cast added otherwise tactics Case (n1,n2) generates (?f x y) and
* refine fails *)
@@ -986,7 +982,7 @@ let elimination_in_clause_scheme id elimclause indclause gl =
errorlabstrm "general_rewrite_in"
(str "Nothing to rewrite in " ++ pr_id id);
tclTHEN
- (tclEVARS elimclause''.hook.sigma)
+ (tclEVARS (evars_of elimclause''.env))
(tclTHENS
(cut new_hyp_typ)
[ (* Try to insert the new hyp at the same place *)
@@ -1667,7 +1663,7 @@ let elim_scheme_type elim t gl =
let clause' =
(* t is inductive, then CUMUL or CONV is irrelevant *)
clenv_unify true CUMUL t (clenv_meta_type clause mv) clause in
- elim_res_pf clause' true gl
+ res_pf clause' ~allow_K:true gl
| _ -> anomaly "elim_scheme_type"
let elim_type t gl =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d2a16dc8e..cbc690c92 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -164,8 +164,8 @@ val cut_and_apply : constr -> tactic
(*s Elimination tactics. *)
-val general_elim : constr with_bindings -> constr with_bindings ->
- ?allow_K:bool -> tactic
+val general_elim :
+ constr with_bindings -> constr with_bindings -> ?allow_K:bool -> tactic
val default_elim : constr with_bindings -> tactic
val simplest_elim : constr -> tactic
val elim : constr with_bindings -> constr with_bindings option -> tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 14:56:53 +0000