aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/include4
-rw-r--r--dev/top_printers.ml4
-rw-r--r--pretyping/clenv.ml93
-rw-r--r--pretyping/clenv.mli131
-rw-r--r--pretyping/evarutil.ml4
-rw-r--r--pretyping/unification.ml10
-rw-r--r--pretyping/unification.mli1
-rw-r--r--proofs/clenvtac.ml28
-rw-r--r--proofs/evar_refiner.ml6
-rw-r--r--proofs/evar_refiner.mli4
-rw-r--r--tactics/auto.ml14
-rw-r--r--tactics/auto.mli8
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/evar_tactics.ml6
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/setoid_replace.ml4
-rw-r--r--tactics/tacticals.ml4
-rw-r--r--tactics/tactics.ml34
-rw-r--r--tactics/tactics.mli2
20 files changed, 206 insertions, 157 deletions
diff --git a/dev/include b/dev/include
index eb370a5d8..bbee6ac74 100644
--- a/dev/include
+++ b/dev/include
@@ -21,8 +21,8 @@
#install_printer (* goal *) prgoal;;
#install_printer (* sigma goal *) prsigmagoal;;
#install_printer (* proof *) pproof;;
-#install_printer (* global_constraints *) prevd;;
-#install_printer (* readable_constraints *) prevc;;
+#install_printer (* evar_map *) prevm;;
+#install_printer (* evar_defs *) prevd;;
#install_printer (* walking_constraints *) prwc;;
#install_printer (* clenv *) prclenv;;
#install_printer (* env *) ppenv;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7f92d64cd..40f7d0da0 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -86,9 +86,9 @@ let prglls glls = pp(pr_glls glls)
let pproof p = pp(print_proof Evd.empty empty_named_context p)
-let prevd evd = pp(pr_decls evd)
+let prevm evd = pp(pr_decls evd)
-let prevc evc = pp(pr_evc evc)
+let prevd evd = prevm(Evarutil.evars_of evd)
let prwc wc = pp(pr_evc wc)
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 7753ec7ed..ef0425e37 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -24,14 +24,21 @@ open Tacexpr
open Tacred
open Pretype_errors
open Evarutil
+open Unification
(* *)
-let get_env evc = Global.env_of_context evc.it
+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 get_env wc = Global.env_of_context wc.it
let w_type_of wc c =
Typing.type_of (get_env wc) wc.sigma c
let w_hnf_constr wc c = hnf_constr (get_env wc) wc.sigma c
let get_concl gl = gl.it.evar_concl
+let mk_wc gls = {it=gls.it.evar_hyps; sigma=gls.sigma}
+
(* Generator of metavariables *)
let new_meta =
let meta_ctr = ref 0 in
@@ -74,6 +81,10 @@ type 'a clausenv = {
type wc = named_context sigma
+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
(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
* mv0, or if one of the free vars on mv1's freelist mentions
@@ -136,15 +147,15 @@ let clenv_environments bound c =
in
clrec (Metamap.empty,Metamap.empty,[]) bound c
-let mk_clenv_from_n wc n (c,cty) =
+let mk_clenv_from_n gls n (c,cty) =
let (namenv,env,args,concl) = clenv_environments n cty in
{ templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
templtyp = mk_freelisted concl;
namenv = namenv;
env = env;
- hook = wc }
+ hook = mk_wc gls }
-let mk_clenv_from wc = mk_clenv_from_n wc None
+let mk_clenv_from gls = mk_clenv_from_n gls None
let subst_clenv f sub clenv =
{ templval = map_fl (subst_mps sub) clenv.templval;
@@ -162,23 +173,23 @@ let clenv_wtactic f clenv =
f (create_evar_defs clenv.hook.sigma, clenv.env) in
{clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=evars_of evd'}}
-let mk_clenv_hnf_constr_type_of wc t =
- mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t))
+let mk_clenv_hnf_constr_type_of gls t =
+ mk_clenv_from gls (t,pf_hnf_constr gls (pf_type_of gls t))
-let mk_clenv_rename_from wc (c,t) =
- mk_clenv_from wc (c,rename_bound_var (get_env wc) [] t)
+let mk_clenv_rename_from gls (c,t) =
+ mk_clenv_from gls (c,rename_bound_var (pf_env gls) [] t)
-let mk_clenv_rename_from_n wc n (c,t) =
- mk_clenv_from_n wc n (c,rename_bound_var (get_env wc) [] t)
-
-let mk_clenv_rename_type_of wc t =
- mk_clenv_from wc (t,rename_bound_var (get_env wc) [] (w_type_of wc t))
+let mk_clenv_rename_from_n gls n (c,t) =
+ mk_clenv_from_n gls n (c,rename_bound_var (pf_env gls) [] t)
+
+let mk_clenv_rename_type_of gls t =
+ mk_clenv_from gls (t,rename_bound_var (pf_env gls) [] (pf_type_of gls t))
-let mk_clenv_rename_hnf_constr_type_of wc t =
- mk_clenv_from wc
- (t,rename_bound_var (get_env wc) [] (w_hnf_constr wc (w_type_of wc t)))
+let mk_clenv_rename_hnf_constr_type_of gls t =
+ mk_clenv_from gls
+ (t,rename_bound_var (pf_env gls) [] (pf_hnf_constr gls (pf_type_of gls t)))
-let mk_clenv_type_of wc t = mk_clenv_from wc (t,w_type_of wc t)
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
let clenv_assign mv rhs clenv =
let rhs_fls = mk_freelisted rhs in
@@ -250,12 +261,12 @@ let clenv_defined clenv mv =
| Clval _ -> true
| Cltyp _ -> false
-let clenv_value clenv mv =
+let clenv_value0 clenv mv =
match Metamap.find mv clenv.env with
| Clval(b,_) -> b
- | Cltyp _ -> failwith "clenv_value"
+ | Cltyp _ -> failwith "clenv_value0"
-let clenv_type clenv mv =
+let clenv_type0 clenv mv =
match Metamap.find mv clenv.env with
| Cltyp b -> b
| Clval(_,b) -> b
@@ -265,10 +276,10 @@ let clenv_template clenv = clenv.templval
let clenv_template_type clenv = clenv.templtyp
let clenv_instance_value clenv mv =
- clenv_instance clenv (clenv_value clenv mv)
+ clenv_instance clenv (clenv_value0 clenv mv)
let clenv_instance_type clenv mv =
- clenv_instance clenv (clenv_type clenv mv)
+ clenv_instance clenv (clenv_type0 clenv mv)
let clenv_instance_template clenv =
clenv_instance clenv (clenv_template clenv)
@@ -291,12 +302,13 @@ let clenv_instance_type_of ce c =
let clenv_unify allow_K cv_pb t1 t2 clenv =
let env = get_env clenv.hook in
- clenv_wtactic (Unification.w_unify allow_K env cv_pb t1 t2) clenv
+ clenv_wtactic (w_unify allow_K env cv_pb t1 t2) clenv
let clenv_unique_resolver allow_K clause gl =
clenv_unify allow_K CUMUL
(clenv_instance_template_type clause) (get_concl gl) clause
+
(* [clenv_bchain mv clenv' clenv]
*
* Resolves the value of "mv" (which must be undefined) in clenv to be
@@ -438,6 +450,27 @@ let clenv_constrain_dep_args hyps_only clause = function
error ("Not the right number of missing arguments (expected "
^(string_of_int (List.length occlist))^")")
+(* [clenv_pose_dependent_evars clenv]
+ * For each dependent evar in the clause-env which does not have a value,
+ * pose a value for it by constructing a fresh evar. We do this in
+ * left-to-right order, so that every evar's type is always closed w.r.t.
+ * metas. *)
+let clenv_pose_dependent_evars clenv =
+ let dep_mvs = clenv_dependent false clenv in
+ List.fold_left
+ (fun clenv mv ->
+ let evar = Evarutil.new_evar_in_sign (get_env clenv.hook) in
+ let (evar_n,_) = destEvar evar in
+ let tY = clenv_instance_type clenv mv in
+ let clenv' =
+ clenv_wtactic (w_Declare (get_env clenv.hook) evar_n tY) clenv in
+ clenv_assign mv evar clenv')
+ clenv
+ dep_mvs
+
+let evar_clenv_unique_resolver clenv gls =
+ clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)
+
let clenv_constrain_missing_args mlist clause =
clenv_constrain_dep_args true clause mlist
@@ -531,19 +564,25 @@ let clenv_constrain_with_bindings bl clause =
(* Clausal environment for an application *)
-let make_clenv_binding_gen n wc (c,t) = function
+let make_clenv_binding_gen n gls (c,t) = function
| ImplicitBindings largs ->
- let clause = mk_clenv_from_n wc n (c,t) in
+ let clause = mk_clenv_from_n gls n (c,t) in
clenv_constrain_dep_args (n <> None) clause largs
| ExplicitBindings lbind ->
- let clause = mk_clenv_rename_from_n wc n (c,t) in
+ let clause = mk_clenv_rename_from_n gls n (c,t) in
clenv_match_args lbind clause
| NoBindings ->
- mk_clenv_from_n wc n (c,t)
+ mk_clenv_from_n gls n (c,t)
let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
let make_clenv_binding = make_clenv_binding_gen None
+
+
+
+
+
+
let pr_clenv clenv =
let pr_name mv =
try
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index d3f36e720..9ed07fc0d 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -23,10 +23,20 @@ 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 :
- Evd.evar_map -> Pretyping.open_constr -> (Termops.metamap * constr)
+ 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.
+ * [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 generally signature (named_context) and a sigma: the
+ * typing context
+ *)
type 'a clausenv = {
templval : constr freelisted;
templtyp : constr freelisted;
@@ -36,70 +46,97 @@ type 'a clausenv = {
type wc = named_context sigma (* for a better reading of the following *)
-(* [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.
- * [env] is the mapping from metavar numbers to their types
- * and values.
- * [hook] is the pointer to the current walking context, for
- * integrating existential vars and metavars. *)
-
-val collect_metas : constr -> metavariable list
-val mk_clenv : 'a -> constr -> 'a clausenv
-val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
-val mk_clenv_from_n : 'a -> int option -> constr * constr -> 'a clausenv
-val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv
-val mk_clenv_rename_from_n : wc -> int option -> constr * constr -> wc clausenv
-val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv
-val mk_clenv_type_of : wc -> constr -> wc clausenv
-
val subst_clenv : (substitution -> 'a -> 'a) ->
substitution -> 'a clausenv -> 'a clausenv
-val clenv_wtactic :
- (evar_defs * meta_map -> evar_defs * meta_map) -> wc clausenv -> wc clausenv
+
+val clenv_nf_meta : wc clausenv -> constr -> constr
+val clenv_meta_type : wc clausenv -> int -> constr
+val clenv_value : wc clausenv -> constr
+val clenv_type : wc clausenv -> constr
+
+val mk_clenv_from : evar_info sigma -> constr * constr -> wc clausenv
+val mk_clenv_from_n :
+ evar_info sigma -> int option -> constr * constr -> wc clausenv
+val mk_clenv_rename_from_n :
+ evar_info sigma -> int option -> constr * constr -> wc clausenv
+val mk_clenv_type_of : evar_info sigma -> constr -> wc clausenv
+
+(***************************************************************)
+(* linking of clenvs *)
val connect_clenv : evar_info sigma -> 'a clausenv -> wc clausenv
-val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv
-val clenv_instance_term : wc clausenv -> constr -> constr
-val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv
-val clenv_template : 'a clausenv -> constr freelisted
-val clenv_template_type : 'a clausenv -> constr freelisted
-val clenv_instance_type : wc clausenv -> metavariable -> constr
-val clenv_instance_template : wc clausenv -> constr
-val clenv_instance_template_type : wc clausenv -> constr
-val clenv_instance : 'a clausenv -> constr freelisted -> constr
-val clenv_type_of : wc clausenv -> constr -> constr
val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
-val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
-(* Unification with clenv *)
-type arg_bindings = (int * constr) list
+(***************************************************************)
+(* Unification with clenvs *)
+(* Unifies two terms in a clenv. The boolean is allow_K (see Unification) *)
val clenv_unify :
bool -> Reductionops.conv_pb -> constr -> constr ->
wc clausenv -> wc clausenv
-val clenv_match_args :
- constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv
-val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
+(* unifies the concl of the goal with the type of the clenv *)
+val clenv_unique_resolver :
+ bool -> wc clausenv -> evar_info sigma -> wc clausenv
+
+(* same as above (allow_K=false) but replaces remaining metas
+ with fresh evars *)
+val evar_clenv_unique_resolver :
+ wc clausenv -> evar_info sigma -> wc clausenv
+
+(***************************************************************)
(* Bindings *)
+
+(* bindings where the key is the position in the template of the
+ clenv (dependent or not). Positions can be negative meaning to
+ start from the rightmost argument of the template. *)
+type arg_bindings = (int * constr) list
+
val clenv_independent : wc clausenv -> metavariable list
-val clenv_dependent : bool -> 'a clausenv -> metavariable list
val clenv_missing : 'a clausenv -> metavariable list
-val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
- constr list -> wc clausenv -> wc clausenv
-(*
-val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
-*)
val clenv_lookup_name : 'a clausenv -> identifier -> metavariable
-val clenv_unique_resolver :
- bool -> wc clausenv -> evar_info sigma -> wc clausenv
+(* defines metas corresponding to the name of the bindings *)
+val clenv_match_args :
+ constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv
+val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
+
+(* start with a clenv to refine with a given term with bindings *)
+
+(* 1- the arity of the lemma is fixed *)
val make_clenv_binding_apply :
- wc -> int -> constr * constr -> types Rawterm.bindings -> wc clausenv
+ evar_info sigma -> int -> constr * constr -> constr Rawterm.bindings ->
+ wc clausenv
val make_clenv_binding :
- wc -> constr * constr -> types Rawterm.bindings -> wc clausenv
+ evar_info sigma -> constr * constr -> constr Rawterm.bindings -> wc clausenv
+(***************************************************************)
(* Pretty-print *)
val pr_clenv : 'a clausenv -> Pp.std_ppcmds
+
+(***************************************************************)
+(* Old or unused stuff... *)
+
+val collect_metas : constr -> metavariable list
+val mk_clenv : 'a -> constr -> 'a clausenv
+
+val mk_clenv_rename_from : evar_info sigma -> constr * constr -> wc clausenv
+val mk_clenv_hnf_constr_type_of : evar_info sigma -> constr -> wc clausenv
+
+val clenv_wtactic :
+ (evar_defs * meta_map -> evar_defs * meta_map) -> wc clausenv -> wc clausenv
+val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv
+val clenv_instance_term : wc clausenv -> constr -> constr
+val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv
+val clenv_template : 'a clausenv -> constr freelisted
+val clenv_template_type : 'a clausenv -> constr freelisted
+val clenv_instance_type : wc clausenv -> metavariable -> constr
+val clenv_instance_template : wc clausenv -> constr
+val clenv_instance_template_type : wc clausenv -> constr
+val clenv_instance : 'a clausenv -> constr freelisted -> constr
+val clenv_type_of : wc clausenv -> constr -> constr
+val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
+val clenv_dependent : bool -> 'a clausenv -> metavariable list
+val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
+ constr list -> wc clausenv -> wc clausenv
+
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 58b3f3ac2..9a4c9cfed 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -279,7 +279,9 @@ let real_clean env isevars ev args rhs =
| Evar (ev,args) ->
let args' = Array.map (subs k) args in
if need_restriction !evd args' then
- begin
+ if Evd.is_defined !evd.evars ev then
+ subs k (existential_value !evd.evars (ev,args'))
+ else begin
let (sigma,rc) = do_restrict_hyps !evd.evars ev args' in
evd :=
{!evd with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 83377449d..4a9cab206 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -51,6 +51,13 @@ let abstract_list_all env sigma typ c l =
type maps = evar_defs * meta_map
+let w_Declare env sp ty (evd,mmap) =
+ 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)
+
(* [w_Define evd sp c]
*
* Defines evar [sp] with term [c] in evar context [evd].
@@ -66,7 +73,8 @@ let w_Define sp c (evd,mmap) =
let spdecl = Evd.map sigma sp in
let env = evar_env spdecl in
let _ =
- try Typing.mcheck env (Evd.rmv sigma sp,Metamap.empty) c spdecl.evar_concl
+ (* Do not consider the metamap because evars may not depend on metas *)
+ try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl
with
Not_found -> error "Instantiation contains unlegal variables"
| (Type_errors.TypeError (e, Type_errors.UnboundVar v))->
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index f033c9e87..02d1918be 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -20,6 +20,7 @@ open Evarutil
type maps = evar_defs * meta_map
+val w_Declare : env -> evar -> types -> maps -> maps
val w_Define : evar -> constr -> maps -> maps
(* The "unique" unification fonction *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 27ae5ebd9..bc50fdd2a 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -31,13 +31,6 @@ open Tacexpr
open Clenv
-let clenv_wtactic wt clenv =
- { templval = clenv.templval;
- templtyp = clenv.templtyp;
- namenv = clenv.namenv;
- env = clenv.env;
- hook = wt clenv.hook }
-
(* This function put casts around metavariables whose type could not be
* infered by the refiner, that is head of applications, predicates and
* subject of Cases.
@@ -94,27 +87,10 @@ let elim_res_pf_THEN_i clenv tac gls =
let clenv' = (clenv_unique_resolver true clenv gls) in
tclTHENLASTn (clenv_refine clenv') (tac clenv') gls
-(* [clenv_pose_dependent_evars clenv]
- * For each dependent evar in the clause-env which does not have a value,
- * pose a value for it by constructing a fresh evar. We do this in
- * left-to-right order, so that every evar's type is always closed w.r.t.
- * metas. *)
-
-let clenv_pose_dependent_evars clenv =
- let dep_mvs = clenv_dependent false clenv in
- List.fold_left
- (fun clenv mv ->
- let evar = Evarutil.new_evar_in_sign (get_env clenv.hook) in
- let (evar_n,_) = destEvar evar in
- let tY = clenv_instance_type clenv mv in
- let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in
- clenv_assign mv evar clenv')
- clenv
- dep_mvs
let e_res_pf clenv gls =
- clenv_refine
- (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls
+ clenv_refine (evar_clenv_unique_resolver clenv gls) gls
+
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 2e2060349..41b910222 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -43,12 +43,6 @@ let extract_decl sp evc =
let restore_decl sp evd evc =
(rc_add evc (sp,evd))
-let w_Declare sp ty (wc : named_context sigma) =
- let _ = Typing.type_of (get_env wc) wc.sigma ty in (* Utile ?? *)
- let sign = get_hyps wc in
- let newdecl = mk_goal sign ty in
- ((rc_add wc (sp,newdecl)): named_context sigma)
-
(******************************************)
(* Instantiation of existential variables *)
(******************************************)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 54646caf8..4766d94cb 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -22,15 +22,11 @@ type wc = named_context sigma (* for a better reading of the following *)
(* Refinement of existential variables. *)
-val rc_of_glsigma : goal sigma -> wc
-
(* A [w_tactic] is a tactic which modifies the a set of evars of which
a goal depend, either by instantiating one, or by declaring a new
dependent goal *)
type w_tactic = wc -> wc
-val w_Declare : evar -> types -> w_tactic
-
val w_refine : evar -> Rawterm.rawconstr -> w_tactic
val instantiate_pf_com :
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 651b976c7..0dc0a9f4c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -44,10 +44,10 @@ open Tacexpr
(****************************************************************************)
type auto_tactic =
- | Res_pf of constr * unit clausenv (* Hint Apply *)
- | ERes_pf of constr * unit clausenv (* Hint EApply *)
+ | Res_pf of constr * wc clausenv (* Hint Apply *)
+ | ERes_pf of constr * wc clausenv (* Hint EApply *)
| Give_exact of constr
- | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
+ | Res_pf_THEN_trivial_fail of constr * wc clausenv (* Hint Immediate *)
| Unfold_nth of global_reference (* Hint Unfold *)
| Extern of glob_tactic_expr (* Hint Extern *)
@@ -186,11 +186,15 @@ let make_exact_entry name (c,cty) =
(head_of_constr_reference (List.hd (head_constr cty)),
{ hname=name; pri=0; pat=None; code=Give_exact c })
+let dummy_goal =
+ {it={evar_hyps=empty_named_context;evar_concl=mkProp;evar_body=Evar_empty};
+ sigma=Evd.empty}
+
let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
let cty = hnf_constr env sigma cty in
match kind_of_term cty with
| Prod _ ->
- let ce = mk_clenv_from () (c,cty) in
+ let ce = mk_clenv_from dummy_goal (c,cty) in
let c' = (clenv_template_type ce).rebus in
let pat = Pattern.pattern_of_constr c' in
let hd = (try head_pattern_bound pat
@@ -256,7 +260,7 @@ let make_extern name pri pat tacast =
let make_trivial env sigma (name,c) =
let t = hnf_constr env sigma (type_of env sigma c) in
let hd = head_of_constr_reference (List.hd (head_constr t)) in
- let ce = mk_clenv_from () (c,t) in
+ let ce = mk_clenv_from dummy_goal (c,t) in
(hd, { hname = name;
pri=1;
pat = Some (Pattern.pattern_of_constr (clenv_template_type ce).rebus);
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 80b807908..18daa6ebe 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -24,10 +24,10 @@ open Vernacexpr
(*i*)
type auto_tactic =
- | Res_pf of constr * unit clausenv (* Hint Apply *)
- | ERes_pf of constr * unit clausenv (* Hint EApply *)
+ | Res_pf of constr * wc clausenv (* Hint Apply *)
+ | ERes_pf of constr * wc clausenv (* Hint EApply *)
| Give_exact of constr
- | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *)
+ | Res_pf_THEN_trivial_fail of constr * wc clausenv (* Hint Immediate *)
| Unfold_nth of global_reference (* Hint Unfold *)
| Extern of Tacexpr.glob_tactic_expr (* Hint Extern *)
@@ -139,7 +139,7 @@ val priority : (int * 'a) list -> 'a list
val default_search_depth : int ref
(* Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : (constr * unit clausenv) -> tactic
+val unify_resolve : (constr * wc clausenv) -> tactic
(* [ConclPattern concl pat tacast]:
if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 700c8fed7..64188d3b8 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -42,7 +42,7 @@ let e_assumption gl =
let e_resolve_with_bindings_tac (c,lbind) gl =
let t = pf_hnf_constr gl (pf_type_of gl c) in
- let clause = make_clenv_binding_apply (rc_of_glsigma gl) (-1) (c,t) lbind in
+ let clause = make_clenv_binding_apply gl (-1) (c,t) lbind in
Clenvtac.e_res_pf clause gl
let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index a58f61550..b5a0370c7 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -66,8 +66,8 @@ let instantiate_tac = function
*)
let let_evar nam typ gls =
- let wc = Refiner.project_with_focus gls in
let sp = Evarutil.new_evar () in
- let wc' = w_Declare sp typ wc in
- let ngls = {gls with sigma = wc'.sigma} 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
Tactics.forward true nam (mkEvar(sp,[||])) ngls
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 7c4456b3d..9a02ba608 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -446,7 +446,7 @@ let raw_inversion inv_kind indbinding id status names gl =
let env = pf_env gl and sigma = project gl in
let c = mkVar id in
let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in
- let indclause = mk_clenv_from (rc_of_glsigma gl) (c,t) in
+ let indclause = mk_clenv_from gl (c,t) in
let indclause' = clenv_constrain_with_bindings indbinding indclause in
let newc = clenv_instance_template indclause' in
let ccl = clenv_instance_template_type indclause' in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 118481547..aa980fd47 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -287,7 +287,7 @@ let add_inversion_lemma_exn na com comsort bool tac =
let lemInv id c gls =
try
- let clause = mk_clenv_type_of (rc_of_glsigma gls) c in
+ 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
with
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 081f135c6..aacaa050e 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -969,9 +969,7 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl =
let general_s_rewrite lft2rgt c gl =
let ctype = pf_type_of gl c in
- let eqclause =
- Clenv.make_clenv_binding
- (Evar_refiner.rc_of_glsigma gl) (c,ctype) Rawterm.NoBindings in
+ let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
let (equiv, args) =
decompose_app (Clenv.clenv_instance_template_type eqclause) in
let rec get_last_two = function
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 72ec0bd2e..fa5eeaef3 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -324,9 +324,9 @@ let general_elim_then_using
elim isrec allnames tac predicate (indbindings,elimbindings) c gl =
let (ity,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
(* applying elimination_scheme just a little modified *)
- let indclause = mk_clenv_from (rc_of_glsigma gl) (c,t) in
+ let indclause = mk_clenv_from gl (c,t) in
let indclause' = clenv_constrain_with_bindings indbindings indclause in
- let elimclause = mk_clenv_from () (elim,pf_type_of gl elim) in
+ let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in
let indmv =
match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
| Meta mv -> mv
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6fe3d75af..d64c90916 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -445,13 +445,12 @@ let apply_with_bindings (c,lbind) gl =
(* 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. *)
- let wc = rc_of_glsigma gl in
let thm_ty0 = nf_betaiota (pf_type_of gl c) in
let rec try_apply thm_ty =
try
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 wc n (c,thm_ty) lbind in
+ let clause = make_clenv_binding_apply gl n (c,thm_ty) lbind in
apply clause gl
with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn ->
let red_thm =
@@ -462,7 +461,7 @@ let apply_with_bindings (c,lbind) gl =
with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) ->
(* Last chance: if the head is a variable, apply may try
second order unification *)
- let clause = make_clenv_binding_apply wc (-1) (c,thm_ty0) lbind in
+ let clause = make_clenv_binding_apply gl (-1) (c,thm_ty0) lbind in
apply clause gl
let apply c = apply_with_bindings (c,NoBindings)
@@ -474,7 +473,7 @@ let apply_list = function
(* Resolution with no reduction on the type *)
let apply_without_reduce c gl =
- let clause = mk_clenv_type_of (rc_of_glsigma gl) c in
+ let clause = mk_clenv_type_of gl c in
res_pf clause gl
(* A useful resolution tactic which, if c:A->B, transforms |- C into
@@ -830,8 +829,7 @@ let rec intros_clearing = function
(* Adding new hypotheses *)
let new_hyp mopt (c,lbind) g =
- let clause =
- make_clenv_binding (rc_of_glsigma g) (c,pf_type_of g c) lbind in
+ let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
let (thd,tstack) = whd_stack (clenv_instance_template clause) in
let nargs = List.length tstack in
let cut_pf =
@@ -926,10 +924,9 @@ let type_clenv_binding wc (c,t) lbind =
let general_elim (c,lbindc) (elimc,lbindelimc) ?(allow_K=true) gl =
let ct = pf_type_of gl c in
let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
- let indclause = make_clenv_binding (rc_of_glsigma gl) (c,t) lbindc in
+ let indclause = make_clenv_binding gl (c,t) lbindc in
let elimt = pf_type_of gl elimc in
- let elimclause =
- make_clenv_binding (rc_of_glsigma gl) (elimc,elimt) lbindelimc in
+ let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in
elimination_clause_scheme elimclause indclause allow_K gl
(* Elimination tactic with bindings but using the default elimination
@@ -971,7 +968,7 @@ let simplest_elim c = default_elim (c,NoBindings)
(* Elimination in hypothesis *)
-let elimination_in_clause_scheme id elimclause indclause =
+let elimination_in_clause_scheme id elimclause indclause gl =
let (hypmv,indmv) =
match clenv_independent elimclause with
[k1;k2] -> (k1,k2)
@@ -981,7 +978,7 @@ let elimination_in_clause_scheme id elimclause indclause =
let hyp = mkVar id in
let hyp_typ = clenv_type_of elimclause' hyp in
let hypclause =
- mk_clenv_from_n elimclause'.hook (Some 0) (hyp, hyp_typ) in
+ mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
let elimclause'' = clenv_fchain hypmv elimclause' hypclause in
let new_hyp_prf = clenv_instance_template elimclause'' in
let new_hyp_typ = clenv_instance_template_type elimclause'' in
@@ -995,16 +992,14 @@ let elimination_in_clause_scheme id elimclause indclause =
[ (* Try to insert the new hyp at the same place *)
tclORELSE (intro_replacing id)
(tclTHEN (clear [id]) (introduction id));
- refine_no_check new_hyp_prf])
+ refine_no_check new_hyp_prf]) gl
let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl =
let ct = pf_type_of gl c in
let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
- let indclause =
- make_clenv_binding (rc_of_glsigma gl) (c,t) lbindc in
+ let indclause = make_clenv_binding gl (c,t) lbindc in
let elimt = pf_type_of gl elimc in
- let elimclause =
- make_clenv_binding (rc_of_glsigma gl) (elimc,elimt) lbindelimc in
+ let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in
elimination_in_clause_scheme id elimclause indclause gl
(* Case analysis tactics *)
@@ -1376,10 +1371,9 @@ let cook_sign hyp0 indvars env =
let induction_tac varname typ ((elimc,lbindelimc),elimt) gl =
let c = mkVar varname in
- let wc = rc_of_glsigma gl in
- let indclause = make_clenv_binding wc (c,typ) NoBindings in
+ let indclause = make_clenv_binding gl (c,typ) NoBindings in
let elimclause =
- make_clenv_binding wc (mkCast (elimc,elimt),elimt) lbindelimc in
+ make_clenv_binding gl (mkCast (elimc,elimt),elimt) lbindelimc in
elimination_clause_scheme elimclause indclause true gl
let make_up_names7 n ind (old_style,cname) =
@@ -1667,7 +1661,7 @@ let simple_destruct = function
*)
let elim_scheme_type elim t gl =
- let clause = mk_clenv_type_of (rc_of_glsigma gl) elim in
+ let clause = mk_clenv_type_of gl elim in
match kind_of_term (last_arg (clenv_template clause).rebus) with
| Meta mv ->
let clause' =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 03e295d8f..d2a16dc8e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -31,7 +31,7 @@ open Rawterm
(*s General functions. *)
-val type_clenv_binding : named_context sigma ->
+val type_clenv_binding : goal sigma ->
constr * constr -> constr bindings -> constr
val string_of_inductive : constr -> string
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 19:44:19 +0000