aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/changes.txt2
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml4
-rw-r--r--pretyping/unification.ml42
-rw-r--r--pretyping/unification.mli6
-rw-r--r--proofs/clenv.ml2
-rw-r--r--proofs/clenvtac.ml2
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/rewrite.ml46
-rw-r--r--tactics/tactics.ml4
10 files changed, 38 insertions, 36 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 035b3ad24..322530e62 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,8 @@
= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
=========================================
+** Functions in unification.ml have now the evar_map coming just after the env
+
** Removal of Tacinterp.constr_of_id **
Use instead either global_reference or construct_reference in constrintern.ml.
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 217a8fe4f..6bcda0097 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -370,8 +370,8 @@ let find_subsubgoal c ctyp skip submetas gls =
let se = Stack.pop stack in
try
let unifier =
- Unification.w_unify env Reduction.CUMUL ~flags:Unification.elim_flags
- ctyp se.se_type se.se_evd in
+ Unification.w_unify env se.se_evd Reduction.CUMUL
+ ~flags:Unification.elim_flags ctyp se.se_type in
if n <= 0 then
{se with
se_evd=meta_assign se.se_meta
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f1fdde390..01d75233b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -927,7 +927,7 @@ let try_resolve_typeclasses env evd flags m n =
error_cannot_unify env evd (m, n)
else evd
-let w_unify_core_0 env with_types cv_pb flags m n evd =
+let w_unify_core_0 env evd with_types cv_pb flags m n =
let (mc1,evd') = retract_coercible_metas evd in
let (sigma,ms,es) = check_types env flags (evd,mc1,[]) m n in
let subst2 =
@@ -936,10 +936,10 @@ let w_unify_core_0 env with_types cv_pb flags m n evd =
let evd = w_merge env with_types flags subst2 in
try_resolve_typeclasses env evd flags m n
-let w_unify_0 env = w_unify_core_0 env false
-let w_typed_unify env = w_unify_core_0 env true
+let w_unify_0 env evd = w_unify_core_0 env evd false
+let w_typed_unify env evd = w_unify_core_0 env evd true
-let w_typed_unify_list env flags f1 l1 f2 l2 evd =
+let w_typed_unify_list env evd flags f1 l1 f2 l2 =
let flags' = { flags with resolve_evars = false } in
let f1,l1,f2,l2 = adjust_app_list_size f1 l1 f2 l2 in
let (mc1,evd') = retract_coercible_metas evd in
@@ -966,12 +966,12 @@ let iter_fail f a =
(* Tries to find an instance of term [cl] in term [op].
Unifies [cl] to every subterm of [op] until it finds a match.
Fails if no match is found *)
-let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd =
+let w_unify_to_subterm env evd ?(flags=default_unify_flags) (op,cl) =
let rec matchrec cl =
let cl = strip_outer_cast cl in
(try
if closed0 cl && not (isEvar cl)
- then w_typed_unify env CONV flags op cl evd,cl
+ then w_typed_unify env evd CONV flags op cl,cl
else error "Bound 1"
with ex when precatchable_exception ex ->
(match kind_of_term cl with
@@ -1026,7 +1026,7 @@ let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd =
(* Tries to find all instances of term [cl] in term [op].
Unifies [cl] to every subterm of [op] and return all the matches.
Fails if no match is found *)
-let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
+let w_unify_to_subterm_all env evd ?(flags=default_unify_flags) (op,cl) =
let return a b =
let (evd,c as a) = a () in
if List.exists (fun (evd',c') -> eq_constr c c') b then b else a :: b
@@ -1051,7 +1051,7 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
let cl = strip_outer_cast cl in
(bind
(if closed0 cl
- then return (fun () -> w_typed_unify env CONV flags op cl evd,cl)
+ then return (fun () -> w_typed_unify env evd CONV flags op cl,cl)
else fail "Bound 1")
(match kind_of_term cl with
| App (f,args) ->
@@ -1087,7 +1087,7 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
else
res
-let w_unify_to_subterm_list env flags hdmeta oplist t evd =
+let w_unify_to_subterm_list env evd flags hdmeta oplist t =
List.fold_right
(fun op (evd,l) ->
let op = whd_meta evd op in
@@ -1098,7 +1098,7 @@ let w_unify_to_subterm_list env flags hdmeta oplist t evd =
let (evd',cl) =
try
(* This is up to delta for subterms w/o metas ... *)
- w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd
+ w_unify_to_subterm env evd ~flags (strip_outer_cast op,t)
with PretypeError (env,_,NoOccurrenceFound _) when
flags.allow_K_in_toplevel_higher_order_unification -> (evd,op)
in
@@ -1116,24 +1116,24 @@ let w_unify_to_subterm_list env flags hdmeta oplist t evd =
oplist
(evd,[])
-let secondOrderAbstraction env flags typ (p, oplist) evd =
+let secondOrderAbstraction env evd flags typ (p, oplist) =
(* Remove delta when looking for a subterm *)
let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in
- let (evd',cllist) = w_unify_to_subterm_list env flags p oplist typ evd in
+ let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
let typp = Typing.meta_type evd' p in
let pred = abstract_list_all env evd' typp typ cllist in
w_merge env false flags (evd',[p,pred,(Conv,TypeProcessed)],[])
-let w_unify2 env flags cv_pb ty1 ty2 evd =
+let w_unify2 env evd flags cv_pb ty1 ty2 =
let c1, oplist1 = whd_stack evd ty1 in
let c2, oplist2 = whd_stack evd ty2 in
match kind_of_term c1, kind_of_term c2 with
| Meta p1, _ ->
(* Find the predicate *)
- secondOrderAbstraction env flags ty2 (p1,oplist1) evd
+ secondOrderAbstraction env evd flags ty2 (p1,oplist1)
| _, Meta p2 ->
(* Find the predicate *)
- secondOrderAbstraction env flags ty1 (p2, oplist2) evd
+ secondOrderAbstraction env evd flags ty1 (p2, oplist2)
| _ -> error "w_unify2"
(* The unique unification algorithm works like this: If the pattern is
@@ -1156,7 +1156,7 @@ let w_unify2 env flags cv_pb ty1 ty2 evd =
Before, second-order was used if the type of Meta(1) and [x:A]t was
convertible and first-order otherwise. But if failed if e.g. the type of
Meta(1) had meta-variables in it. *)
-let w_unify env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
+let w_unify env evd cv_pb ?(flags=default_unify_flags) ty1 ty2 =
let hd1,l1 = whd_stack evd ty1 in
let hd2,l2 = whd_stack evd ty2 in
match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
@@ -1164,22 +1164,22 @@ let w_unify env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
| (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
when List.length l1 = List.length l2 ->
(try
- w_typed_unify_list env flags hd1 l1 hd2 l2 evd
+ w_typed_unify_list env evd flags hd1 l1 hd2 l2
with ex when precatchable_exception ex ->
try
- w_unify2 env flags cv_pb ty1 ty2 evd
+ w_unify2 env evd flags cv_pb ty1 ty2
with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e)
(* Second order case *)
| (Meta _, true, _, _ | _, _, Meta _, true) ->
(try
- w_unify2 env flags cv_pb ty1 ty2 evd
+ w_unify2 env evd flags cv_pb ty1 ty2
with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e
| ex when precatchable_exception ex ->
try
- w_typed_unify_list env flags hd1 l1 hd2 l2 evd
+ w_typed_unify_list env evd flags hd1 l1 hd2 l2
with ex' when precatchable_exception ex' ->
raise ex)
(* General case: try first order *)
- | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd
+ | _ -> w_typed_unify env evd cv_pb flags ty1 ty2
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index cc781c871..d28451177 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -33,16 +33,16 @@ val elim_no_delta_flags : unify_flags
(** The "unique" unification fonction *)
val w_unify :
- env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -> evar_map
+ env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map
(** [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 -> ?flags:unify_flags -> constr * constr -> evar_map -> evar_map * constr
+ env -> evar_map -> ?flags:unify_flags -> constr * constr -> evar_map * constr
val w_unify_to_subterm_all :
- env -> ?flags:unify_flags -> constr * constr -> evar_map -> (evar_map * constr) list
+ env -> evar_map -> ?flags:unify_flags -> constr * constr -> (evar_map * constr) list
val w_unify_meta_types : env -> ?flags:unify_flags -> evar_map -> evar_map
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 6e6fff96d..d06c6f2e6 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -267,7 +267,7 @@ let clenv_dependent ce = clenv_dependent_gen false ce
let clenv_unify ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
{ clenv with
- evd = w_unify ~flags clenv.env cv_pb t1 t2 clenv.evd }
+ evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
{ clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index ec9aada73..ff84a343b 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -119,7 +119,7 @@ let fail_quick_unif_flags = {
let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
let env = pf_env gls in
let evd = create_goal_evar_defs (project gls) in
- let evd' = w_unify env CONV ~flags m n evd in
+ let evd' = w_unify env evd CONV ~flags m n in
tclIDTAC {it = gls.it; sigma = evd'}
let unify ?(flags=fail_quick_unif_flags) m gls =
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 8ccf751c4..13f8784f5 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -246,7 +246,7 @@ type hypinfo = {
let evd_convertible env evd x y =
try
- ignore(Unification.w_unify ~flags:Unification.elim_flags env Reduction.CONV x y evd); true
+ ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true
(* try ignore(Evarconv.the_conv_x env x y evd); true *)
with _ -> false
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d21d3e767..2d4268e60 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -131,8 +131,8 @@ let instantiate_lemma_all frzevars env sigma gl c ty l l2r concl =
in
let flags = make_flags frzevars sigma rewrite_unif_flags eqclause in
let occs =
- Unification.w_unify_to_subterm_all ~flags env
- ((if l2r then c1 else c2),concl) eqclause.evd
+ Unification.w_unify_to_subterm_all ~flags env eqclause.evd
+ ((if l2r then c1 else c2),concl)
in List.map try_occ occs
let instantiate_lemma env sigma gl c ty l l2r concl =
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index c908f7188..1595ded2d 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1021,7 +1021,7 @@ module Strategies =
with _ -> error "fold: the term is not unfoldable !"
in
try
- let sigma = Unification.w_unify env CONV ~flags:Unification.elim_flags unfolded t sigma in
+ let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
let c' = Evarutil.nf_evar sigma c in
Some (Some { rew_car = ty; rew_from = t; rew_to = c';
rew_prf = RewCast DEFAULTcast;
@@ -1771,13 +1771,13 @@ let unification_rewrite flags l2r c1 c2 cl car rel but gl =
(* ~flags:(false,true) to allow to mark occurrences that must not be
rewritten simply by replacing them with let-defined definitions
in the context *)
- Unification.w_unify_to_subterm ~flags:rewrite_unif_flags env ((if l2r then c1 else c2),but) cl.evd
+ Unification.w_unify_to_subterm ~flags:rewrite_unif_flags env cl.evd ((if l2r then c1 else c2),but)
with
Pretype_errors.PretypeError _ ->
(* ~flags:(true,true) to make Ring work (since it really
exploits conversion) *)
Unification.w_unify_to_subterm ~flags:flags
- env ((if l2r then c1 else c2),but) cl.evd
+ env cl.evd ((if l2r then c1 else c2),but)
in
let evd' = Typeclasses.resolve_typeclasses ~fail:false env evd' in
let cl' = {cl with evd = evd'} in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2f0eaf82e..692622f32 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1704,7 +1704,7 @@ let default_matching_flags sigma = {
let make_pattern_test env sigma0 (sigma,c) =
let flags = default_matching_flags sigma0 in
let matching_fun t =
- try let sigma = w_unify env Reduction.CONV ~flags c t sigma in Some(sigma,t)
+ try let sigma = w_unify env sigma Reduction.CONV ~flags c t in Some(sigma,t)
with _ -> raise NotUnifiable in
let merge_fun c1 c2 =
match c1, c2 with
@@ -3531,6 +3531,6 @@ let unify ?(state=full_transparent_state) x y gl =
modulo_delta = state;
modulo_conv_on_closed_terms = Some state}
in
- let evd = w_unify (pf_env gl) Reduction.CONV ~flags x y (project gl)
+ let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y
in tclEVARS evd gl
with _ -> tclFAIL 0 (str"Not unifiable") gl
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 13:10:19 +0000