aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ltac/g_eqdecide.ml42
-rw-r--r--proofs/tacmach.ml2
-rw-r--r--proofs/tacmach.mli4
-rw-r--r--tactics/eqdecide.ml35
-rw-r--r--tactics/eqdecide.mli2
-rw-r--r--tactics/hipattern.ml5
-rw-r--r--tactics/hipattern.mli2
7 files changed, 29 insertions, 23 deletions
diff --git a/ltac/g_eqdecide.ml4 b/ltac/g_eqdecide.ml4
index 905653281..6a49ea830 100644
--- a/ltac/g_eqdecide.ml4
+++ b/ltac/g_eqdecide.ml4
@@ -23,5 +23,5 @@ TACTIC EXTEND decide_equality
END
TACTIC EXTEND compare
-| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
+| [ "compare" constr(c1) constr(c2) ] -> [ compare (EConstr.of_constr c1) (EConstr.of_constr c2) ]
END
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b732e5b9d..aa54e4f9b 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -23,6 +23,8 @@ open Context.Named.Declaration
module NamedDecl = Context.Named.Declaration
+let compute env sigma c = EConstr.of_constr (compute env sigma c)
+
let re_sig it gc = { it = it; sigma = gc; }
(**************************************************************)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index cfbfe12b1..340c7addc 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -69,7 +69,7 @@ val pf_nf : goal sigma -> EConstr.constr -> constr
val pf_nf_betaiota : goal sigma -> EConstr.constr -> constr
val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types
val pf_reduce_to_atomic_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types
-val pf_compute : goal sigma -> EConstr.constr -> constr
+val pf_compute : goal sigma -> EConstr.constr -> EConstr.constr
val pf_unfoldn : (occurrences * evaluable_global_reference) list
-> goal sigma -> EConstr.constr -> constr
@@ -127,7 +127,7 @@ module New : sig
val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types
val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr
- val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr
+ val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr
val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index be9a34239..a96656d3a 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -16,6 +16,7 @@ open Util
open Names
open Namegen
open Term
+open EConstr
open Declarations
open Tactics
open Tacticals.New
@@ -52,7 +53,6 @@ open Coqlib
*)
let clear_last =
- let open EConstr in
Proofview.tclEVARMAP >>= fun sigma ->
(onLastHyp (fun c -> (clear [destVar sigma c])))
@@ -70,14 +70,14 @@ let choose_noteq eqonleft =
let mkBranches c1 c2 =
tclTHENLIST
[generalize [c2];
- Simple.elim (EConstr.of_constr c1);
+ Simple.elim c1;
intros;
onLastHyp Simple.case;
clear_last;
intros]
let discrHyp id =
- let c = { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma } in
+ let c = { delayed = fun env sigma -> Sigma.here (mkVar id, NoBindings) sigma } in
let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in
Tacticals.New.tclDELAYEDWITHHOLES false c tac
@@ -89,7 +89,9 @@ let solveNoteqBranch side =
(* Constructs the type {c1=c2}+{~c1=c2} *)
let make_eq () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
+(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
+let build_coq_not () = EConstr.of_constr (build_coq_not ())
+let build_coq_sumbool () = EConstr.of_constr (build_coq_sumbool ())
let mkDecideEqGoal eqonleft op rectype c1 c2 =
let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in
@@ -116,7 +118,7 @@ let rec rewrite_and_clear hyps = match hyps with
| [] -> Proofview.tclUNIT ()
| id :: hyps ->
tclTHENLIST [
- Equality.rewriteLR (EConstr.mkVar id);
+ Equality.rewriteLR (mkVar id);
clear [id];
rewrite_and_clear hyps;
]
@@ -125,7 +127,7 @@ let eqCase tac =
tclTHEN intro (onLastHypId tac)
let injHyp id =
- let c = { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma } in
+ let c = { delayed = fun env sigma -> Sigma.here (mkVar id, NoBindings) sigma } in
let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in
Tacticals.New.tclDELAYEDWITHHOLES false c tac
@@ -137,7 +139,7 @@ let diseqCase hyps eqonleft =
(tclTHEN (rewrite_and_clear (List.rev hyps))
(tclTHEN (red_in_concl)
(tclTHEN (intro_using absurd)
- (tclTHEN (Simple.apply (EConstr.mkVar diseq))
+ (tclTHEN (Simple.apply (mkVar diseq))
(tclTHEN (injHyp absurd)
(full_trivial []))))))))
@@ -160,9 +162,9 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
]
| a1 :: largs, a2 :: rargs ->
Proofview.Goal.enter { enter = begin fun gl ->
- let rectype = pf_unsafe_type_of gl (EConstr.of_constr a1) in
+ let rectype = pf_unsafe_type_of gl a1 in
+ let rectype = EConstr.of_constr rectype in
let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
- let decide = EConstr.of_constr decide in
let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
let subtacs =
if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
@@ -181,7 +183,7 @@ let solveEqBranch rectype =
match_eqdec sigma concl >>= fun (eqonleft,op,lhs,rhs,_) ->
let (mib,mip) = Global.lookup_inductive rectype in
let nparams = mib.mind_nparams in
- let getargs l = List.skipn nparams (snd (decompose_app l)) in
+ let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in
let rargs = getargs rhs
and largs = getargs lhs in
solveArg [] eqonleft op largs rargs
@@ -194,7 +196,7 @@ let solveEqBranch rectype =
(* The tactic Decide Equality *)
-let hd_app c = match kind_of_term c with
+let hd_app sigma c = match EConstr.kind sigma c with
| App (h,_) -> h
| _ -> c
@@ -206,13 +208,13 @@ let decideGralEquality =
let concl = EConstr.of_constr concl in
let sigma = project gl in
match_eqdec sigma concl >>= fun (eqonleft,_,c1,c2,typ) ->
- let headtyp = hd_app (pf_compute gl (EConstr.of_constr typ)) in
- begin match kind_of_term headtyp with
+ let headtyp = hd_app sigma (pf_compute gl typ) in
+ begin match EConstr.kind sigma headtyp with
| Ind (mi,_) -> Proofview.tclUNIT mi
| _ -> tclZEROMSG (Pp.str"This decision procedure only works for inductive objects.")
end >>= fun rectype ->
(tclTHEN
- (mkBranches c1 (EConstr.of_constr c2))
+ (mkBranches c1 c2)
(tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
end }
end
@@ -227,7 +229,6 @@ let decideEqualityGoal = tclTHEN intros decideGralEquality
let decideEquality rectype =
Proofview.Goal.enter { enter = begin fun gl ->
let decide = mkGenDecideEqGoal rectype gl in
- let decide = EConstr.of_constr decide in
(tclTHENS (cut decide) [default_auto;decideEqualityGoal])
end }
@@ -236,9 +237,9 @@ let decideEquality rectype =
let compare c1 c2 =
Proofview.Goal.enter { enter = begin fun gl ->
- let rectype = pf_unsafe_type_of gl (EConstr.of_constr c1) in
+ let rectype = pf_unsafe_type_of gl c1 in
+ let rectype = EConstr.of_constr rectype in
let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
- let decide = EConstr.of_constr decide in
(tclTHENS (cut decide)
[(tclTHEN intro
(tclTHEN (onLastHyp simplest_case) clear_last));
diff --git a/tactics/eqdecide.mli b/tactics/eqdecide.mli
index cb48a5bcc..dca1780b7 100644
--- a/tactics/eqdecide.mli
+++ b/tactics/eqdecide.mli
@@ -14,4 +14,4 @@
val decideEqualityGoal : unit Proofview.tactic
-val compare : Constr.t -> Constr.t -> unit Proofview.tactic
+val compare : EConstr.t -> EConstr.t -> unit Proofview.tactic
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 36ed589b9..9e78ff323 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -548,7 +548,10 @@ let match_eqdec sigma t =
false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in
match Id.Map.bindings subst with
| [(_,typ);(_,c1);(_,c2)] ->
- eqonleft, Universes.constr_of_global (Lazy.force op), c1, c2, typ
+ let typ = EConstr.of_constr typ in
+ let c1 = EConstr.of_constr c1 in
+ let c2 = EConstr.of_constr c2 in
+ eqonleft, EConstr.of_constr (Universes.constr_of_global (Lazy.force op)), c1, c2, typ
| _ -> anomaly (Pp.str "Unexpected pattern")
(* Patterns "~ ?" and "? -> False" *)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index c061c50f0..65ba0aad0 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -143,7 +143,7 @@ val is_matching_sigma : evar_map -> constr -> bool
(** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
[t,u,T] and a boolean telling if equality is on the left side *)
-val match_eqdec : evar_map -> constr -> bool * Constr.constr * Constr.constr * Constr.constr * Constr.constr
+val match_eqdec : evar_map -> constr -> bool * constr * constr * constr * constr
(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
val dest_nf_eq : ([ `NF ], 'r) Proofview.Goal.t -> constr -> (constr * constr * constr)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 11:53:36 +0000