aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/instances.ml20
-rw-r--r--plugins/firstorder/instances.mli2
-rw-r--r--plugins/firstorder/sequent.ml4
-rw-r--r--plugins/firstorder/sequent.mli2
-rw-r--r--plugins/firstorder/unify.ml14
-rw-r--r--plugins/firstorder/unify.mli6
6 files changed, 25 insertions, 23 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 834e4251d3..f13901c36d 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -57,12 +57,12 @@ let make_simple_atoms seq=
| None->[]
in {negative=seq.latoms;positive=ratoms}
-let do_sequent sigma setref triv id seq i dom atoms=
+let do_sequent env sigma setref triv id seq i dom atoms=
let flag=ref true in
let phref=ref triv in
let do_atoms a1 a2 =
let do_pair t1 t2 =
- match unif_atoms sigma i dom t1 t2 with
+ match unif_atoms env sigma i dom t1 t2 with
None->()
| Some (Phantom _) ->phref:=true
| Some c ->flag:=false;setref:=IS.add (c,id) !setref in
@@ -72,16 +72,16 @@ let do_sequent sigma setref triv id seq i dom atoms=
do_atoms atoms (make_simple_atoms seq);
!flag && !phref
-let match_one_quantified_hyp sigma setref seq lf=
+let match_one_quantified_hyp env sigma setref seq lf=
match lf.pat with
Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
- if do_sequent sigma setref triv lf.id seq i dom lf.atoms then
+ if do_sequent env sigma setref triv lf.id seq i dom lf.atoms then
setref:=IS.add ((Phantom dom),lf.id) !setref
| _ -> anomaly (Pp.str "can't happen.")
-let give_instances sigma lf seq=
+let give_instances env sigma lf seq=
let setref=ref IS.empty in
- List.iter (match_one_quantified_hyp sigma setref seq) lf;
+ List.iter (match_one_quantified_hyp env sigma setref seq) lf;
IS.elements !setref
(* collector for the engine *)
@@ -129,9 +129,10 @@ let left_instance_tac (inst,id) continue seq=
let open EConstr in
Proofview.Goal.enter begin fun gl ->
let sigma = project gl in
+ let env = Proofview.Goal.env gl in
match inst with
Phantom dom->
- if lookup sigma (id,None) seq then
+ if lookup env sigma (id,None) seq then
tclFAIL 0 (Pp.str "already done")
else
tclTHENS (cut dom)
@@ -148,7 +149,7 @@ let left_instance_tac (inst,id) continue seq=
tclTRY assumption]
| Real((m,t),_)->
let c = (m, EConstr.to_constr sigma t) in
- if lookup sigma (id,Some c) seq then
+ if lookup env sigma (id,Some c) seq then
tclFAIL 0 (Pp.str "already done")
else
let special_generalize=
@@ -205,7 +206,8 @@ let instance_tac inst=
let quantified_tac lf backtrack continue seq =
Proofview.Goal.enter begin fun gl ->
- let insts=give_instances (project gl) lf seq in
+ let env = Proofview.Goal.env gl in
+ let insts=give_instances env (project gl) lf seq in
tclORELSE
(tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
backtrack
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index c0f4c78ff3..08c2c4d916 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -13,7 +13,7 @@ open Rules
val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t
-val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t ->
+val give_instances : Environ.env -> Evd.evar_map -> Formula.t list -> Sequent.t ->
(Unify.instance * GlobRef.t) list
val quantified_tac : Formula.t list -> seqtac with_backtracking
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 7bf13fd25b..3dd5059e5d 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -109,7 +109,7 @@ let deepen seq={seq with depth=seq.depth-1}
let record item seq={seq with history=History.add item seq.history}
-let lookup sigma item seq=
+let lookup env sigma item seq=
History.mem item seq.history ||
match item with
(_,None)->false
@@ -117,7 +117,7 @@ let lookup sigma item seq=
let p (id2,o)=
match o with
None -> false
- | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
+ | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general env sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
History.exists p seq.history
let add_formula env sigma side nam t seq =
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 3a5da6ad14..bba89c823c 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -39,7 +39,7 @@ val deepen: t -> t
val record: h_item -> t -> t
-val lookup: Evd.evar_map -> h_item -> t -> bool
+val lookup: Environ.env -> Evd.evar_map -> h_item -> t -> bool
val add_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> constr -> t -> t
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index e58e80116d..9c3debe48f 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -29,7 +29,7 @@ let subst_meta subst t =
let subst = List.map (fun (m, c) -> (m, EConstr.Unsafe.to_constr c)) subst in
EConstr.of_constr (subst_meta subst (EConstr.Unsafe.to_constr t))
-let unif evd t1 t2=
+let unif env evd t1 t2=
let bige=Queue.create ()
and sigma=ref [] in
let bind i t=
@@ -46,8 +46,8 @@ let unif evd t1 t2=
Queue.add (t1,t2) bige;
try while true do
let t1,t2=Queue.take bige in
- let nt1=head_reduce (whd_betaiotazeta evd t1)
- and nt2=head_reduce (whd_betaiotazeta evd t2) in
+ let nt1=head_reduce (whd_betaiotazeta env evd t1)
+ and nt2=head_reduce (whd_betaiotazeta env evd t2) in
match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with
Meta i,Meta j->
if not (Int.equal i j) then
@@ -123,9 +123,9 @@ let mk_rel_inst evd t=
in
let nt=renum_rec 0 t in (!new_rel - 1,nt)
-let unif_atoms evd i dom t1 t2=
+let unif_atoms env evd i dom t1 t2=
try
- let t=Int.List.assoc i (unif evd t1 t2) in
+ let t=Int.List.assoc i (unif env evd t1 t2) in
if isMeta evd t then Some (Phantom dom)
else Some (Real(mk_rel_inst evd t,value evd i t1))
with
@@ -136,11 +136,11 @@ let renum_metas_from k n t= (* requires n = max (free_rels t) *)
let l=List.init n (fun i->mkMeta (k+i)) in
substl l t
-let more_general evd (m1,t1) (m2,t2)=
+let more_general env evd (m1,t1) (m2,t2)=
let mt1=renum_metas_from 0 m1 t1
and mt2=renum_metas_from m1 m2 t2 in
try
- let sigma=unif evd mt1 mt2 in
+ let sigma=unif env evd mt1 mt2 in
let p (n,t)= n<m1 || isMeta evd t in
List.for_all p sigma
with UFAIL(_,_)->false
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index 71e786eb90..c6767f04ac 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -13,12 +13,12 @@ open EConstr
exception UFAIL of constr*constr
-val unif : Evd.evar_map -> constr -> constr -> (int*constr) list
+val unif : Environ.env -> Evd.evar_map -> constr -> constr -> (int*constr) list
type instance=
Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
| Phantom of constr (* domaine de quantification *)
-val unif_atoms : Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option
+val unif_atoms : Environ.env -> Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option
-val more_general : Evd.evar_map -> (int*constr) -> (int*constr) -> bool
+val more_general : Environ.env -> Evd.evar_map -> (int*constr) -> (int*constr) -> bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:37:50 +0000