aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml1
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/class_tactics.ml13
-rw-r--r--tactics/contradiction.ml3
-rw-r--r--tactics/declare.ml93
-rw-r--r--tactics/declare.mli8
-rw-r--r--tactics/eauto.ml10
-rw-r--r--tactics/elim.ml9
-rw-r--r--tactics/elimschemes.ml4
-rw-r--r--tactics/eqdecide.ml15
-rw-r--r--tactics/equality.ml81
-rw-r--r--tactics/hints.ml19
-rw-r--r--tactics/hints.mli2
-rw-r--r--tactics/hipattern.ml27
-rw-r--r--tactics/hipattern.mli4
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/pfedit.ml3
-rw-r--r--tactics/proof_global.ml1
-rw-r--r--tactics/redexpr.ml2
-rw-r--r--tactics/tacticals.ml6
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tactics/tactics.ml315
23 files changed, 313 insertions, 315 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9c1a975330..1dde820075 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -177,7 +177,6 @@ let global_info_auto = ref false
let add_option ls refe =
Goptions.(declare_bool_option
{ optdepr = false;
- optname = String.concat " " ls;
optkey = ls;
optread = (fun () -> !refe);
optwrite = (:=) refe })
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index cd6f445503..1bbcca8827 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -238,7 +238,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
in
try
let others,(c1,c2) = split_last_two args in
- let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in
+ let ty1, ty2 = Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2 in
(* XXX: It looks like mk_clenv_from_env should be fixed instead? *)
let open EConstr in
let hyp_ty = Unsafe.to_constr ty in
@@ -261,7 +261,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
| None -> None
let find_applied_relation ?loc metas env sigma c left2right =
- let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in
+ let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in
match decompose_applied_relation metas env sigma c ctype left2right with
| Some c -> c
| None ->
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index f8cb8870ea..28feeecb86 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -83,8 +83,6 @@ open Goptions
let () =
declare_bool_option
{ optdepr = false;
- optname = "do typeclass search avoiding eta-expansions " ^
- " in proof terms (expensive)";
optkey = ["Typeclasses";"Limit";"Intros"];
optread = get_typeclasses_limit_intros;
optwrite = set_typeclasses_limit_intros; }
@@ -92,7 +90,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "during typeclass resolution, solve instances according to their dependency order";
optkey = ["Typeclasses";"Dependency";"Order"];
optread = get_typeclasses_dependency_order;
optwrite = set_typeclasses_dependency_order; }
@@ -100,7 +97,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "use iterative deepening strategy";
optkey = ["Typeclasses";"Iterative";"Deepening"];
optread = get_typeclasses_iterative_deepening;
optwrite = set_typeclasses_iterative_deepening; }
@@ -108,7 +104,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "compat";
optkey = ["Typeclasses";"Filtered";"Unification"];
optread = get_typeclasses_filtered_unification;
optwrite = set_typeclasses_filtered_unification; }
@@ -116,7 +111,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "debug output for typeclasses proof search";
optkey = ["Typeclasses";"Debug"];
optread = get_typeclasses_debug;
optwrite = set_typeclasses_debug; }
@@ -124,7 +118,6 @@ let () =
let _ =
declare_int_option
{ optdepr = false;
- optname = "verbosity of debug output for typeclasses proof search";
optkey = ["Typeclasses";"Debug";"Verbosity"];
optread = get_typeclasses_verbose;
optwrite = set_typeclasses_verbose; }
@@ -132,7 +125,6 @@ let _ =
let () =
declare_int_option
{ optdepr = false;
- optname = "depth for typeclasses proof search";
optkey = ["Typeclasses";"Depth"];
optread = get_typeclasses_depth;
optwrite = set_typeclasses_depth; }
@@ -1202,10 +1194,9 @@ let autoapply c i =
in
let flags = auto_unif_flags
(Hints.Hint_db.transparent_state hintdb) in
- let cty = Tacmach.New.pf_unsafe_type_of gl c in
+ let cty = Tacmach.New.pf_get_type_of gl c in
let ce = mk_clenv_from gl (c,cty) in
- unify_e_resolve false flags gl
- ((c,cty,Univ.ContextSet.empty),0,ce) <*>
+ unify_e_resolve false flags gl ((c,cty,Univ.ContextSet.empty),0,ce) <*>
Proofview.tclEVARMAP >>= (fun sigma ->
let sigma = Typeclasses.make_unresolvables
(fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 1f5a6380fd..c7b6998c8c 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -110,8 +110,7 @@ let contradiction_term (c,lbind as cl) =
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
- let type_of = Tacmach.New.pf_unsafe_type_of gl in
- let typ = type_of c in
+ let typ = Tacmach.New.pf_get_type_of gl c in
let _, ccl = splay_prod env sigma typ in
if is_empty_type env sigma ccl then
Tacticals.New.tclTHEN
diff --git a/tactics/declare.ml b/tactics/declare.ml
index da4de3df77..ce2f3ec2c5 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -130,8 +130,8 @@ let dummy_constant cst = {
let classify_constant cst = Substitute (dummy_constant cst)
-let (inConstant : constant_obj -> obj) =
- declare_object { (default_object "CONSTANT") with
+let (objConstant : constant_obj Libobject.Dyn.tag) =
+ declare_object_full { (default_object "CONSTANT") with
cache_function = cache_constant;
load_function = load_constant;
open_function = open_constant;
@@ -139,6 +139,8 @@ let (inConstant : constant_obj -> obj) =
subst_function = ident_subst_function;
discharge_function = discharge_constant }
+let inConstant v = Libobject.Dyn.Easy.inj v objConstant
+
let update_tables c =
Impargs.declare_constant_implicits c;
Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c)
@@ -158,6 +160,18 @@ let register_side_effect (c, role) =
| None -> ()
| Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|]
+let get_roles export eff =
+ let map c =
+ let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
+ (c, role)
+ in
+ List.map map export
+
+let export_side_effects eff =
+ let export = Global.export_private_constants eff.Evd.seff_private in
+ let export = get_roles export eff in
+ List.iter register_side_effect export
+
let record_aux env s_ty s_bo =
let open Environ in
let in_ty = keep_hyps env s_ty in
@@ -276,13 +290,6 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo
opaque_entry_universes = univs;
}
-let get_roles export eff =
- let map c =
- let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
- (c, role)
- in
- List.map map export
-
let feedback_axiom () = Feedback.(feedback AddedAxiom)
let is_unsafe_typing_flags () =
@@ -291,37 +298,36 @@ let is_unsafe_typing_flags () =
let define_constant ~name cd =
(* Logically define the constant and its subproofs, no libobject tampering *)
- let export, decl, unsafe = match cd with
- | DefinitionEntry de ->
- (* We deal with side effects *)
- if not de.proof_entry_opaque then
- (* This globally defines the side-effects in the environment. *)
- let body, eff = Future.force de.proof_entry_body in
- let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in
- let export = get_roles export eff in
- let de = { de with proof_entry_body = Future.from_val (body, ()) } in
- let cd = Entries.DefinitionEntry (cast_proof_entry de) in
- export, ConstantEntry cd, false
- else
- let map (body, eff) = body, eff.Evd.seff_private in
- let body = Future.chain de.proof_entry_body map in
- let de = { de with proof_entry_body = body } in
- let de = cast_opaque_proof_entry EffectEntry de in
- [], OpaqueEntry de, false
- | ParameterEntry e ->
- [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
- | PrimitiveEntry e ->
- [], ConstantEntry (Entries.PrimitiveEntry e), false
+ let decl, unsafe = match cd with
+ | DefinitionEntry de ->
+ (* We deal with side effects *)
+ if not de.proof_entry_opaque then
+ let body, eff = Future.force de.proof_entry_body in
+ (* This globally defines the side-effects in the environment
+ and registers their libobjects. *)
+ let () = export_side_effects eff in
+ let de = { de with proof_entry_body = Future.from_val (body, ()) } in
+ let cd = Entries.DefinitionEntry (cast_proof_entry de) in
+ ConstantEntry cd, false
+ else
+ let map (body, eff) = body, eff.Evd.seff_private in
+ let body = Future.chain de.proof_entry_body map in
+ let de = { de with proof_entry_body = body } in
+ let de = cast_opaque_proof_entry EffectEntry de in
+ OpaqueEntry de, false
+ | ParameterEntry e ->
+ ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
+ | PrimitiveEntry e ->
+ ConstantEntry (Entries.PrimitiveEntry e), false
in
let kn = Global.add_constant name decl in
if unsafe || is_unsafe_typing_flags() then feedback_axiom();
- kn, export
+ kn
let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
let () = check_exists name in
- let kn, export = define_constant ~name cd in
- (* Register the libobjects attached to the constants and its subproofs *)
- let () = List.iter register_side_effect export in
+ let kn = define_constant ~name cd in
+ (* Register the libobjects attached to the constants *)
let () = register_constant kn kind local in
kn
@@ -357,12 +363,14 @@ type variable_declaration =
(* This object is only for things which iterate over objects to find
variables (only Prettyp.print_context AFAICT) *)
-let inVariable : unit -> obj =
- declare_object { (default_object "VARIABLE") with
+let objVariable : unit Libobject.Dyn.tag =
+ declare_object_full { (default_object "VARIABLE") with
classify_function = (fun () -> Dispose)}
+let inVariable v = Libobject.Dyn.Easy.inj v objVariable
+
let declare_variable ~name ~kind d =
- (* Constr raisonne sur les noms courts *)
+ (* Variables are distinguished by only short names *)
if Decls.variable_exists name then
raise (AlreadyDeclared (None, name));
@@ -373,10 +381,8 @@ let declare_variable ~name ~kind d =
| SectionLocalDef (de) ->
(* The body should already have been forced upstream because it is a
section-local definition, but it's not enforced by typing *)
- let (body, eff) = Future.force de.proof_entry_body in
- let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in
- let eff = get_roles export eff in
- let () = List.iter register_side_effect eff in
+ let ((body, uctx), eff) = Future.force de.proof_entry_body in
+ let () = export_side_effects eff in
let poly, univs = match de.proof_entry_universes with
| Monomorphic_entry uctx -> false, uctx
| Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
@@ -497,4 +503,9 @@ module Internal = struct
; proof_entry_type = Some typ
}, args
+ type nonrec constant_obj = constant_obj
+
+ let objVariable = objVariable
+ let objConstant = objConstant
+
end
diff --git a/tactics/declare.mli b/tactics/declare.mli
index c646d2f85b..00c1e31717 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -131,7 +131,8 @@ val check_exists : Id.t -> unit
(* Used outside this module only in indschemes *)
exception AlreadyDeclared of (string option * Id.t)
-(* For legacy support, do not use *)
+(** {6 For legacy support, do not use} *)
+
module Internal : sig
val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
@@ -145,4 +146,9 @@ module Internal : sig
val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
+ type constant_obj
+
+ val objConstant : constant_obj Libobject.Dyn.tag
+ val objVariable : unit Libobject.Dyn.tag
+
end
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 361215bf38..9a1e6a6736 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -32,11 +32,13 @@ let eauto_unif_flags = auto_flags_of_state TransparentState.full
let e_give_exact ?(flags=eauto_unif_flags) c =
Proofview.Goal.enter begin fun gl ->
- let t1 = Tacmach.New.pf_unsafe_type_of gl c in
+ let sigma, t1 = Tacmach.New.pf_type_of gl c in
let t2 = Tacmach.New.pf_concl gl in
- let sigma = Tacmach.New.project gl in
if occur_existential sigma t1 || occur_existential sigma t2 then
- Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
+ Tacticals.New.tclTHENLIST
+ [Proofview.Unsafe.tclEVARS sigma;
+ Clenvtac.unify ~flags t1;
+ exact_no_check c]
else exact_check c
end
@@ -329,7 +331,6 @@ let global_info_eauto = ref false
let () =
Goptions.(declare_bool_option
{ optdepr = false;
- optname = "Debug Eauto";
optkey = ["Debug";"Eauto"];
optread = (fun () -> !global_debug_eauto);
optwrite = (:=) global_debug_eauto })
@@ -337,7 +338,6 @@ let () =
let () =
Goptions.(declare_bool_option
{ optdepr = false;
- optname = "Info Eauto";
optkey = ["Info";"Eauto"];
optread = (fun () -> !global_info_eauto);
optwrite = (:=) global_info_eauto })
diff --git a/tactics/elim.ml b/tactics/elim.ml
index ea61b8e4df..379a8d5401 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -80,14 +80,11 @@ let up_to_delta = ref false (* true *)
let general_decompose recognizer c =
Proofview.Goal.enter begin fun gl ->
- let type_of = pf_unsafe_type_of gl in
- let env = pf_env gl in
- let sigma = project gl in
- let typc = type_of c in
+ let typc = pf_get_type_of gl c in
tclTHENS (cut typc)
[ tclTHEN (intro_using tmphyp_name)
(onLastHypId
- (ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma))
+ (ifOnHyp recognizer (general_decompose_aux recognizer)
(fun id -> clear [id])));
exact_no_check c ]
end
@@ -136,7 +133,7 @@ let induction_trailer abs_i abs_j bargs =
(onLastHypId
(fun id ->
Proofview.Goal.enter begin fun gl ->
- let idty = pf_unsafe_type_of gl (mkVar id) in
+ let idty = pf_get_type_of gl (mkVar id) in
let fvty = global_vars (pf_env gl) (project gl) idty in
let possible_bring_hyps =
(List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index d6fda00ad8..6cdb24965d 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -49,14 +49,14 @@ let optimize_non_type_induction_scheme kind dep sort ind =
let sigma = Evd.minimize_universes sigma in
(Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma)
else
- let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+ let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
let sigma, c = build_induction_scheme env sigma pind dep sort in
(c, Evd.evar_universe_context sigma)
let build_induction_scheme_in_type dep sort ind =
let env = Global.env () in
let sigma = Evd.from_env env in
- let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+ let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
let sigma, c = build_induction_scheme env sigma pind dep sort in
c, Evd.evar_universe_context sigma
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index bdfd200988..a82b26f428 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -195,13 +195,13 @@ let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with
]
| a1 :: largs, a2 :: rargs ->
Proofview.Goal.enter begin fun gl ->
- let rectype = pf_unsafe_type_of gl a1 in
+ let sigma, rectype = pf_type_of gl a1 in
let decide = mk rectype a1 a2 in
let tac hyp = solveArg (hyp :: hyps) eqonleft mk largs rargs in
let subtacs =
if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
- (tclTHENS (elim_type decide) subtacs)
+ tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (elim_type decide) subtacs)
end
| _ -> invalid_arg "List.fold_right2"
@@ -274,11 +274,12 @@ let compare c1 c2 =
pf_constr_of_global (lib_ref "core.eq.type") >>= fun eqc ->
pf_constr_of_global (lib_ref "core.not.type") >>= fun notc ->
Proofview.Goal.enter begin fun gl ->
- let rectype = pf_unsafe_type_of gl c1 in
+ let sigma, rectype = pf_type_of gl c1 in
let ops = (opc,eqc,notc) in
let decide = mkDecideEqGoal true ops rectype c1 c2 in
- (tclTHENS (cut decide)
- [(tclTHEN intro
- (tclTHEN (onLastHyp simplest_case) clear_last));
- decideEquality rectype ops])
+ tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ (tclTHENS (cut decide)
+ [(tclTHEN intro
+ (tclTHEN (onLastHyp simplest_case) clear_last));
+ decideEquality rectype ops])
end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 96b61b6994..7393454ba9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -72,7 +72,6 @@ let use_injection_in_context = function
let () =
declare_bool_option
{ optdepr = false;
- optname = "injection in context";
optkey = ["Structural";"Injection"];
optread = (fun () -> !injection_in_context) ;
optwrite = (fun b -> injection_in_context := b) }
@@ -356,7 +355,7 @@ let find_elim hdcncl lft2rgt dep cls ot =
Proofview.Goal.enter_one begin fun gl ->
let sigma = project gl in
let is_global_exists gr c =
- Coqlib.has_ref gr && Termops.is_global sigma (Coqlib.lib_ref gr) c
+ Coqlib.has_ref gr && isRefX sigma (Coqlib.lib_ref gr) c
in
let inccl = Option.is_empty cls in
let env = Proofview.Goal.env gl in
@@ -734,7 +733,6 @@ let keep_proof_equalities_for_injection = ref false
let () =
declare_bool_option
{ optdepr = false;
- optname = "injection on prop arguments";
optkey = ["Keep";"Proof";"Equalities"];
optread = (fun () -> !keep_proof_equalities_for_injection) ;
optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
@@ -1062,14 +1060,14 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let onEquality with_evars tac (c,lbindc) =
Proofview.Goal.enter begin fun gl ->
- let type_of = pf_unsafe_type_of gl in
let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
- let t = type_of c in
+ let t = pf_get_type_of gl c in
let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in
let eqn = clenv_type eq_clause' in
- let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
+ (* FIXME evar leak *)
+ let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in
tclTHEN
(Proofview.Unsafe.tclEVARS eq_clause'.evd)
(tac (eq,eqn,eq_args) eq_clause')
@@ -1165,7 +1163,7 @@ let minimal_free_rels_rec env sigma =
let rec minimalrec_free_rels_rec prev_rels (c,cty) =
let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
let combined_rels = Int.Set.union prev_rels direct_rels in
- let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i)))
+ let folder rels i = snd (minimalrec_free_rels_rec rels (c, get_type_of env sigma (mkRel i)))
in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
in minimalrec_free_rels_rec Int.Set.empty
@@ -1210,7 +1208,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let rec sigrec_clausal_form sigma siglen p_i =
if Int.equal siglen 0 then
(* is the default value typable with the expected type *)
- let dflt_typ = unsafe_type_of env sigma dflt in
+ let sigma, dflt_typ = type_of env sigma dflt in
try
let sigma = Evarconv.unify_leq_delay env sigma dflt_typ p_i in
let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
@@ -1224,29 +1222,21 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let sigma, ev = Evarutil.new_evar env sigma a in
let rty = beta_applist sigma (p_i_minus_1,[ev]) in
let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in
- let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in
- match evopt with
- | Some w ->
- let w_type = unsafe_type_of env sigma w in
- begin match Evarconv.unify_leq_delay env sigma w_type a with
- | sigma ->
- let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
- sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
- | exception Evarconv.UnableToUnify _ ->
- user_err Pp.(str "Cannot solve a unification problem.")
- end
- | None ->
- (* This at least happens if what has been detected as a
- dependency is not one; use an evasive error message;
- even if the problem is upwards: unification should be
- tried in the first place in make_iterated_tuple instead
- of approximatively computing the free rels; then
- unsolved evars would mean not binding rel *)
- user_err Pp.(str "Cannot solve a unification problem.")
+ if EConstr.isEvar sigma ev then
+ (* This at least happens if what has been detected as a
+ dependency is not one; use an evasive error message;
+ even if the problem is upwards: unification should be
+ tried in the first place in make_iterated_tuple instead
+ of approximatively computing the free rels; then
+ unsolved evars would mean not binding rel *)
+ user_err Pp.(str "Cannot solve a unification problem.")
+ else
+ let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
+ sigma, applist(exist_term,[a;p_i_minus_1;ev;tuple_tail])
in
let sigma = Evd.clear_metas sigma in
let sigma, scf = sigrec_clausal_form sigma siglen ty in
- sigma, Evarutil.nf_evar sigma scf
+ sigma, Evarutil.nf_evar sigma scf
(* The problem is to build a destructor (a generalization of the
predecessor) which, when applied to a term made of constructors
@@ -1319,7 +1309,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
sigma, (tuple,tuplety,dfltval)
let rec build_injrec env sigma dflt c = function
- | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c)
+ | [] -> make_iterated_tuple env sigma dflt (c,get_type_of env sigma c)
| ((sp,cnum),argnum)::l ->
try
let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1341,17 +1331,17 @@ let inject_if_homogenous_dependent_pair ty =
Proofview.Goal.enter begin fun gl ->
try
let sigma = Tacmach.New.project gl in
- let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
+ let eq,u,(t,t1,t2) = pf_apply find_this_eq_data_decompose gl ty in
(* fetch the informations of the pair *)
let sigTconstr = Coqlib.(lib_ref "core.sigT.type") in
let existTconstr = Coqlib.lib_ref "core.sigT.intro" in
(* check whether the equality deals with dep pairs or not *)
let eqTypeDest = fst (decompose_app sigma t) in
- if not (Termops.is_global sigma sigTconstr eqTypeDest) then raise Exit;
+ if not (isRefX sigma sigTconstr eqTypeDest) then raise Exit;
let hd1,ar1 = decompose_app_vect sigma t1 and
hd2,ar2 = decompose_app_vect sigma t2 in
- if not (Termops.is_global sigma existTconstr hd1) then raise Exit;
- if not (Termops.is_global sigma existTconstr hd2) then raise Exit;
+ if not (isRefX sigma existTconstr hd1) then raise Exit;
+ if not (isRefX sigma existTconstr hd2) then raise Exit;
let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
(* check if the user has declared the dec principle *)
(* and compare the fst arguments of the dep pair *)
@@ -1360,7 +1350,7 @@ let inject_if_homogenous_dependent_pair ty =
if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind &&
pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
check_required_library ["Coq";"Logic";"Eqdep_dec"];
- let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
+ let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in
let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
(* cut with the good equality and prove the requested goal *)
@@ -1603,7 +1593,7 @@ let cutSubstInConcl l2r eqn =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
+ let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in
let typ = pf_concl gl in
let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
@@ -1620,7 +1610,7 @@ let cutSubstInHyp l2r eqn id =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
+ let (lbeq,u,(t,e1,e2)) = pf_apply find_eq_data_decompose gl eqn in
let typ = pf_get_hyp_typ id gl in
let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
@@ -1694,14 +1684,13 @@ let regular_subst_tactic = ref true
let () =
declare_bool_option
{ optdepr = false;
- optname = "more regular behavior of tactic subst";
optkey = ["Regular";"Subst";"Tactic"];
optread = (fun () -> !regular_subst_tactic);
optwrite = (:=) regular_subst_tactic }
let restrict_to_eq_and_identity eq = (* compatibility *)
- if not (is_global (lib_ref "core.eq.type") eq) &&
- not (is_global (lib_ref "core.identity.type") eq)
+ if not (Constr.isRefX (lib_ref "core.eq.type") eq) &&
+ not (Constr.isRefX (lib_ref "core.identity.type") eq)
then raise Constr_matching.PatternMatchingFailure
exception FoundHyp of (Id.t * constr * bool)
@@ -1715,7 +1704,7 @@ let is_eq_x gl x d =
| _ -> false
in
let c = pf_nf_evar gl (NamedDecl.get_type d) in
- let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
+ let (_,lhs,rhs) = pi3 (pf_apply find_eq_data_decompose gl c) in
if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true));
if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false))
with Constr_matching.PatternMatchingFailure ->
@@ -1812,7 +1801,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
let find_equations gl =
let env = Proofview.Goal.env gl in
let sigma = project gl in
- let find_eq_data_decompose = find_eq_data_decompose gl in
+ let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
let select_equation_name decl =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
@@ -1837,7 +1826,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
Proofview.Goal.enter begin fun gl ->
let sigma = project gl in
let env = Proofview.Goal.env gl in
- let find_eq_data_decompose = find_eq_data_decompose gl in
+ let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
let _,_,(_,x,y) = find_eq_data_decompose c in
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
@@ -1863,7 +1852,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
let-ins *)
Proofview.Goal.enter begin fun gl ->
let sigma = project gl in
- let find_eq_data_decompose = find_eq_data_decompose gl in
+ let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
let test (_,c) =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose c in
@@ -1887,19 +1876,19 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
let cond_eq_term_left c t gl =
try
- let (_,x,_) = pi3 (find_eq_data_decompose gl t) in
+ let (_,x,_) = pi3 (pf_apply find_eq_data_decompose gl t) in
if pf_conv_x gl c x then true else failwith "not convertible"
with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
let cond_eq_term_right c t gl =
try
- let (_,_,x) = pi3 (find_eq_data_decompose gl t) in
+ let (_,_,x) = pi3 (pf_apply find_eq_data_decompose gl t) in
if pf_conv_x gl c x then false else failwith "not convertible"
with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
let cond_eq_term c t gl =
try
- let (_,x,y) = pi3 (find_eq_data_decompose gl t) in
+ let (_,x,y) = pi3 (pf_apply find_eq_data_decompose gl t) in
if pf_conv_x gl c x then true
else if pf_conv_x gl c y then false
else failwith "not convertible"
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7b3797119a..86aa046586 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -26,7 +26,6 @@ open Libnames
open Smartlocate
open Termops
open Inductiveops
-open Typing
open Typeclasses
open Pattern
open Patternops
@@ -206,7 +205,6 @@ let write_warn_hint = function
let () =
Goptions.(declare_string_option
{ optdepr = false;
- optname = "behavior of non-imported hints";
optkey = ["Loose"; "Hint"; "Behavior"];
optread = read_warn_hint;
optwrite = write_warn_hint;
@@ -966,16 +964,17 @@ let make_mode ref m =
let make_trivial env sigma poly ?(name=PathAny) r =
let c,ctx = fresh_global_or_constr env sigma poly r in
let sigma = Evd.merge_context_set univ_flexible sigma ctx in
- let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
+ let t = hnf_constr env sigma (Retyping.get_type_of env sigma c) in
let hd = head_constr sigma t in
let ce = mk_clenv_from_env env sigma None (c,t) in
- (Some hd, { pri=1;
- poly = poly;
- pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
- name = name;
- db = None;
- secvars = secvars_of_constr env sigma c;
- code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
+ (Some hd,
+ { pri=1;
+ poly = poly;
+ pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
+ name = name;
+ db = None;
+ secvars = secvars_of_constr env sigma c;
+ code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 2a9b71387e..9c9f0b7708 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -160,6 +160,8 @@ module Hint_db :
val iter : (GlobRef.t option ->
hint_mode array list -> full_hint list -> unit) -> t -> unit
+ val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a
+
val use_dn : t -> bool
val transparent_state : t -> TransparentState.t
val set_transparent_state : t -> TransparentState.t -> t
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 90a9a7acd9..5404404af5 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -19,7 +19,6 @@ open Inductiveops
open Constr_matching
open Coqlib
open Declarations
-open Tacmach.New
open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
@@ -432,10 +431,10 @@ let match_eq sigma eqn (ref, hetero) =
in
match EConstr.kind sigma eqn with
| App (c, [|t; x; y|]) ->
- if not hetero && Termops.is_global sigma ref c then PolymorphicLeibnizEq (t, x, y)
+ if not hetero && isRefX sigma ref c then PolymorphicLeibnizEq (t, x, y)
else raise PatternMatchingFailure
| App (c, [|t; x; t'; x'|]) ->
- if hetero && Termops.is_global sigma ref c then HeterogenousEq (t, x, t', x')
+ if hetero && isRefX sigma ref c then HeterogenousEq (t, x, t', x')
else raise PatternMatchingFailure
| _ -> raise PatternMatchingFailure
@@ -452,26 +451,26 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *)
let hd,u = destInd sigma (fst (destApp sigma eqn)) in
d,u,k
-let extract_eq_args gl = function
+let extract_eq_args env sigma = function
| MonomorphicLeibnizEq (e1,e2) ->
- let t = pf_unsafe_type_of gl e1 in (t,e1,e2)
+ let t = Retyping.get_type_of env sigma e1 in (t,e1,e2)
| PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
| HeterogenousEq (t1,e1,t2,e2) ->
- if pf_conv_x gl t1 t2 then (t1,e1,e2)
+ if Reductionops.is_conv env sigma t1 t2 then (t1,e1,e2)
else raise PatternMatchingFailure
-let find_eq_data_decompose gl eqn =
- let (lbeq,u,eq_args) = find_eq_data (project gl) eqn in
- (lbeq,u,extract_eq_args gl eq_args)
+let find_eq_data_decompose env sigma eqn =
+ let (lbeq,u,eq_args) = find_eq_data sigma eqn in
+ (lbeq,u,extract_eq_args env sigma eq_args)
-let find_this_eq_data_decompose gl eqn =
+let find_this_eq_data_decompose env sigma eqn =
let (lbeq,u,eq_args) =
try (*first_match (match_eq eqn) inversible_equalities*)
- find_eq_data (project gl) eqn
+ find_eq_data sigma eqn
with PatternMatchingFailure ->
user_err (str "No primitive equality found.") in
let eq_args =
- try extract_eq_args gl eq_args
+ try extract_eq_args env sigma eq_args
with PatternMatchingFailure ->
user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in
(lbeq,u,eq_args)
@@ -480,9 +479,9 @@ let find_this_eq_data_decompose gl eqn =
let match_sigma env sigma ex =
match EConstr.kind sigma ex with
- | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sig.intro") f ->
+ | App (f, [| a; p; car; cdr |]) when isRefX sigma (lib_ref "core.sig.intro") f ->
build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr)
- | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sigT.intro") f ->
+ | App (f, [| a; p; car; cdr |]) when isRefX sigma (lib_ref "core.sigT.intro") f ->
build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr)
| _ -> raise PatternMatchingFailure
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 803305a1ca..0000f81d3f 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -122,11 +122,11 @@ val match_with_equation:
(** Match terms [eq A t u], [identity A t u] or [JMeq A t A u]
Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
-val find_eq_data_decompose : Proofview.Goal.t -> constr ->
+val find_eq_data_decompose : Environ.env -> evar_map -> constr ->
coq_eq_data * EInstance.t * (types * constr * constr)
(** Idem but fails with an error message instead of PatternMatchingFailure *)
-val find_this_eq_data_decompose : Proofview.Goal.t -> constr ->
+val find_this_eq_data_decompose : Environ.env -> evar_map -> constr ->
coq_eq_data * EInstance.t * (types * constr * constr)
(** A variant that returns more informative structure on the equality found *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index be0421d42d..4239fc8bc0 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -352,7 +352,7 @@ let dest_nf_eq env sigma t = match EConstr.kind sigma t with
| App (r, [| t; x; y |]) ->
let open Reductionops in
let eq = Coqlib.lib_ref "core.eq.type" in
- if EConstr.is_global sigma eq r then
+ if isRefX sigma eq r then
(t, whd_all env sigma x, whd_all env sigma y)
else user_err Pp.(str "Not an equality.")
| _ ->
@@ -464,7 +464,7 @@ let raw_inversion inv_kind id status names =
let concl = Proofview.Goal.concl gl in
let c = mkVar id in
let (ind, t) =
- try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
+ try pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl c)
with UserError _ ->
let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in
CErrors.user_err msg
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index cf58c9306c..def4af1ae8 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -259,7 +259,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac =
let lemInv id c =
Proofview.Goal.enter begin fun gls ->
try
- let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in
+ let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in
let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
with
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 3c9803432a..72204e1d24 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -17,7 +17,6 @@ open Evd
let use_unification_heuristics_ref = ref true
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname = "Solve unification constraints at every \".\"";
optkey = ["Solve";"Unification";"Constraints"];
optread = (fun () -> !use_unification_heuristics_ref);
optwrite = (fun a -> use_unification_heuristics_ref:=a);
@@ -27,7 +26,7 @@ let use_unification_heuristics () = !use_unification_heuristics_ref
exception NoSuchGoal
let () = CErrors.register_handler begin function
- | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
+ | NoSuchGoal -> Pp.(str "No such goal.")
| _ -> raise CErrors.Unhandled
end
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index b1fd34e43c..4c470519d6 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -143,7 +143,6 @@ let private_poly_univs =
let b = ref true in
let _ = Goptions.(declare_bool_option {
optdepr = false;
- optname = "use private polymorphic universes for Qed constants";
optkey = ["Private";"Polymorphic";"Universes"];
optread = (fun () -> !b);
optwrite = ((:=) b);
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index fc7b126ee5..a30c877435 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -56,8 +56,6 @@ let strong_cbn flags =
let simplIsCbn = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Plug the simpl tactic to the new cbn mechanism";
optkey = ["SimplIsCbn"];
optread = (fun () -> !simplIsCbn);
optwrite = (fun a -> simplIsCbn:=a);
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ed7ab9164a..58d2097dea 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -587,7 +587,7 @@ module New = struct
let ifOnHyp pred tac1 tac2 id =
Proofview.Goal.enter begin fun gl ->
let typ = Tacmach.New.pf_get_hyp_typ id gl in
- if pred (id,typ) then
+ if pf_apply pred gl (id,typ) then
tac1 id
else
tac2 id
@@ -633,7 +633,7 @@ module New = struct
(Proofview.Goal.enter begin fun gl ->
let indclause = mk_clenv_from gl (c, t) in
(* applying elimination_scheme just a little modified *)
- let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim) in
+ let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim) in
let indmv =
match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
| Meta mv -> mv
@@ -741,7 +741,7 @@ module New = struct
let elimination_then tac c =
Proofview.Goal.enter begin fun gl ->
- let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
+ let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in
let isrec,mkelim =
match (Global.lookup_mind (fst (fst ind))).mind_record with
| NotRecord -> true,gl_make_elim
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 31d26834d6..4b93b81d1c 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -222,7 +222,7 @@ module New : sig
val nLastDecls : Proofview.Goal.t -> int -> named_context
- val ifOnHyp : (Id.t * types -> bool) ->
+ val ifOnHyp : (Environ.env -> evar_map -> Id.t * types -> bool) ->
(Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) ->
Id.t -> unit Proofview.tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f6f7c71dfd..8371da76b2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -47,6 +47,9 @@ open Context.Named.Declaration
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
+let tclEVARS = Proofview.Unsafe.tclEVARS
+let tclEVARSTHEN sigma t = Proofview.tclTHEN (tclEVARS sigma) t
+
let inj_with_occurrences e = (AllOccurrences,e)
let typ_of env sigma c =
@@ -64,7 +67,6 @@ let use_clear_hyp_by_default () = !clear_hyp_by_default
let () =
declare_bool_option
{ optdepr = false;
- optname = "default clearing of hypotheses after use";
optkey = ["Default";"Clearing";"Used";"Hypotheses"];
optread = (fun () -> !clear_hyp_by_default) ;
optwrite = (fun b -> clear_hyp_by_default := b) }
@@ -80,7 +82,6 @@ let accept_universal_lemma_under_conjunctions () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "trivial unification in tactics applying under conjunctions";
optkey = ["Universal";"Lemma";"Under";"Conjunction"];
optread = (fun () -> !universal_lemma_under_conjunctions) ;
optwrite = (fun b -> universal_lemma_under_conjunctions := b) }
@@ -99,7 +100,6 @@ let use_bracketing_last_or_and_intro_pattern () =
let () =
declare_bool_option
{ optdepr = true;
- optname = "bracketing last or-and introduction pattern";
optkey = ["Bracketing";"Last";"Introduction";"Pattern"];
optread = (fun () -> !bracketing_last_or_and_intro_pattern);
optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) }
@@ -151,11 +151,12 @@ let convert_concl ~check ty k =
Refine.refine ~typecheck:false begin fun sigma ->
let sigma =
if check then begin
- ignore (Typing.unsafe_type_of env sigma ty);
+ let sigma, _ = Typing.type_of env sigma ty in
match Reductionops.infer_conv env sigma ty conclty with
| None -> error "Not convertible."
| Some sigma -> sigma
- end else sigma in
+ end else sigma
+ in
let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ty in
let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
(sigma, ans)
@@ -849,12 +850,13 @@ let change_on_subterm ~check cv_pb deep t where env sigma c =
change_and_check Reduction.CONV mayneedglobalcheck true (t subst)
else
fun env sigma _c -> t subst env sigma) env sigma c in
- if !mayneedglobalcheck then
+ let sigma = if !mayneedglobalcheck then
begin
- try ignore (Typing.unsafe_type_of env sigma c)
+ try fst (Typing.type_of env sigma c)
with e when catchable_exception e ->
error "Replacement would lead to an ill-typed term."
- end;
+ end else sigma
+ in
(sigma, c)
let change_in_concl ~check occl t =
@@ -1308,30 +1310,23 @@ let cut c =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
- let relevance =
- try
- (* Backward compat: ensure that [c] is well-typed. Plus we
- need to know the relevance *)
- let typ = Typing.unsafe_type_of env sigma c in
- let typ = whd_all env sigma typ in
- match EConstr.kind sigma typ with
- | Sort s -> Some (Sorts.relevance_of_sort (ESorts.kind sigma s))
- | _ -> None
- with e when Pretype_errors.precatchable_exception e -> None
- in
- match relevance with
- | Some r ->
+ (* Backward compat: ensure that [c] is well-typed. Plus we need to
+ know the relevance *)
+ match Typing.sort_of env sigma c with
+ | exception e when Pretype_errors.precatchable_exception e ->
+ Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
+ | sigma, s ->
+ let r = Sorts.relevance_of_sort s in
let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
(* Backward compat: normalize [c]. *)
let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
- Refine.refine ~typecheck:false begin fun h ->
- let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in
- let (h, x) = Evarutil.new_evar env h c in
- let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
- (h, f)
- end
- | None ->
- Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ (Refine.refine ~typecheck:false begin fun h ->
+ let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in
+ let (h, x) = Evarutil.new_evar env h c in
+ let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
+ (h, f)
+ end)
end
let error_uninstantiated_metas t clenv =
@@ -1533,16 +1528,19 @@ exception IsNonrec
let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite
-let find_ind_eliminator ind s gl =
- let env = Proofview.Goal.env gl in
+let find_ind_eliminator env sigma ind s =
let gr = lookup_eliminator env ind s in
- Tacmach.New.pf_apply Evd.fresh_global gl gr
+ Evd.fresh_global env sigma gr
let find_eliminator c gl =
- let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let concl = Proofview.Goal.concl gl in
+ let sigma, t = Typing.type_of env sigma c in
+ let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
if is_nonrec ind then raise IsNonrec;
- let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
- evd, { elimindex = None; elimbody = (c,NoBindings) }
+ let sigma, c = find_ind_eliminator env sigma ind (Retyping.get_sort_family_of env sigma concl) in
+ sigma, { elimindex = None; elimbody = (c,NoBindings) }
let default_elim with_evars clear_flag (c,_ as cx) =
Proofview.tclORELSE
@@ -1928,18 +1926,20 @@ let apply_in_delayed_once ?(respect_opaque = false) with_delta
let cut_and_apply c =
Proofview.Goal.enter begin fun gl ->
- let sigma = Tacmach.New.project gl in
- match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
- | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 ->
- let concl = Proofview.Goal.concl gl in
- let env = Tacmach.New.pf_env gl in
- Refine.refine ~typecheck:false begin fun sigma ->
- let typ = mkProd (make_annot Anonymous Sorts.Relevant, c2, concl) in
- let (sigma, f) = Evarutil.new_evar env sigma typ in
- let (sigma, x) = Evarutil.new_evar env sigma c1 in
- (sigma, mkApp (f, [|mkApp (c, [|x|])|]))
- end
- | _ -> error "lapply needs a non-dependent product."
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let concl = Proofview.Goal.concl gl in
+ let sigma, t = Typing.type_of env sigma c in
+ match EConstr.kind sigma (hnf_constr env sigma t) with
+ | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 ->
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ (Refine.refine ~typecheck:false begin fun sigma ->
+ let typ = mkProd (make_annot Anonymous Sorts.Relevant, c2, concl) in
+ let (sigma, f) = Evarutil.new_evar env sigma typ in
+ let (sigma, x) = Evarutil.new_evar env sigma c1 in
+ (sigma, mkApp (f, [|mkApp (c, [|x|])|]))
+ end)
+ | _ -> error "lapply needs a non-dependent product."
end
(********************************************************************)
@@ -2285,8 +2285,8 @@ let intro_decomp_eq_function = ref (fun _ -> failwith "Not implemented")
let declare_intro_decomp_eq f = intro_decomp_eq_function := f
-let my_find_eq_data_decompose gl t =
- try Some (find_eq_data_decompose gl t)
+let my_find_eq_data_decompose env sigma t =
+ try Some (find_eq_data_decompose env sigma t)
with e when is_anomaly e
(* Hack in case equality is not yet defined... one day, maybe,
known equalities will be dynamically registered *)
@@ -2296,13 +2296,15 @@ let my_find_eq_data_decompose gl t =
let intro_decomp_eq ?loc l thin tac id =
Proofview.Goal.enter begin fun gl ->
let c = mkVar id in
- let t = Tacmach.New.pf_unsafe_type_of gl c in
- let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
- match my_find_eq_data_decompose gl t with
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma, t = Typing.type_of env sigma c in
+ let _,t = reduce_to_quantified_ind env sigma t in
+ match my_find_eq_data_decompose env sigma t with
| Some (eq,u,eq_args) ->
!intro_decomp_eq_function
- (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l)
- (eq,t,eq_args) (c, t)
+ (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l)
+ (eq,t,eq_args) (c, t)
| None ->
Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
end
@@ -2310,16 +2312,19 @@ let intro_decomp_eq ?loc l thin tac id =
let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
Proofview.Goal.enter begin fun gl ->
let c = mkVar id in
- let t = Tacmach.New.pf_unsafe_type_of gl c in
- let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma, t = Typing.type_of env sigma c in
+ let (ind,t) = reduce_to_quantified_ind env sigma t in
let branchsigns = compute_constructor_signatures ~rec_flag:false ind in
let nv_with_let = Array.map List.length branchsigns in
let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
let ll = get_and_check_or_and_pattern ?loc ll branchsigns in
- Tacticals.New.tclTHENLASTn
- (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
- (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
- nv_with_let ll)
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ (Tacticals.New.tclTHENLASTn
+ (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
+ (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
+ nv_with_let ll))
end
let rewrite_hyp_then assert_style with_evars thin l2r id tac =
@@ -2333,9 +2338,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
- let type_of = Tacmach.New.pf_unsafe_type_of gl in
- let whd_all = Tacmach.New.pf_apply whd_all gl in
- let t = whd_all (type_of (mkVar id)) in
+ let sigma, t = Typing.type_of env sigma (mkVar id) in
+ let t = whd_all env sigma t in
let eqtac, thin = match match_with_equality_type env sigma t with
| Some (hdcncl,[_;lhs;rhs]) ->
if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then
@@ -2361,7 +2365,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]),
thin in
(* Skip the side conditions of the rewriting step *)
- Tacticals.New.tclTHENFIRST eqtac (tac thin)
+ tclEVARSTHEN sigma (Tacticals.New.tclTHENFIRST eqtac (tac thin))
end
let prepare_naming ?loc = function
@@ -3392,8 +3396,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
let id = match EConstr.kind sigma c with
| Var id -> id
| _ ->
- let type_of = Tacmach.New.pf_unsafe_type_of gl in
- id_of_name_using_hdchar env sigma (type_of c) Anonymous in
+ let type_of = Tacmach.New.pf_get_type_of gl in
+ id_of_name_using_hdchar env sigma (type_of c) Anonymous
+ in
let x = fresh_id_in_env avoid id env in
Tacticals.New.tclTHEN
(letin_tac None (Name x) c None allHypsAndConcl)
@@ -3794,15 +3799,15 @@ let is_defined_variable env id =
env |> lookup_named id |> is_local_def
let abstract_args gl generalize_vars dep id defined f args =
- let open Tacmach.New in
let open Context.Rel.Declaration in
let sigma = ref (Tacmach.New.project gl) in
let env = Tacmach.New.pf_env gl in
let concl = Tacmach.New.pf_concl gl in
+ let hyps = Proofview.Goal.hyps gl in
let dep = dep || local_occur_var !sigma id concl in
let avoid = ref Id.Set.empty in
let get_id name =
- let id = new_fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in
+ let id = fresh_id_in_env !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") env in
avoid := Id.Set.add id !avoid; id
in
(* Build application generalized w.r.t. the argument plus the necessary eqs.
@@ -3811,14 +3816,14 @@ let abstract_args gl generalize_vars dep id defined f args =
eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *)
*)
- let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg =
+ let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars) arg =
let name, ty_relevance, ty, arity =
let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in
let decl = List.hd rel in
RelDecl.get_name decl, RelDecl.get_relevance decl, RelDecl.get_type decl, c
in
- let argty = Tacmach.New.pf_unsafe_type_of gl arg in
- let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
+ let sigma', argty = Typing.type_of env !sigma arg in
+ let sigma', ty = Evarsolve.refresh_universes (Some true) env sigma' ty in
let () = sigma := sigma' in
let lenctx = List.length ctx in
let liftargty = lift lenctx argty in
@@ -3826,7 +3831,7 @@ let abstract_args gl generalize_vars dep id defined f args =
match EConstr.kind !sigma arg with
| Var id when not (is_defined_variable env id) && leq && not (Id.Set.mem id nongenvars) ->
(subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls,
- Id.Set.add id nongenvars, Id.Set.remove id vars, env)
+ Id.Set.add id nongenvars, Id.Set.remove id vars)
| _ ->
let name = get_id name in
let decl = LocalAssum (make_annot (Name name) ty_relevance, ty) in
@@ -3848,7 +3853,7 @@ let abstract_args gl generalize_vars dep id defined f args =
let refls = refl :: refls in
let argvars = ids_of_constr !sigma vars arg in
(arity, ctx, push_rel decl ctxenv, c', args, eqs, refls,
- nongenvars, Id.Set.union argvars vars, env)
+ nongenvars, Id.Set.union argvars vars)
in
let f', args' = decompose_indapp !sigma f args in
let dogen, f', args' =
@@ -3862,15 +3867,16 @@ let abstract_args gl generalize_vars dep id defined f args =
true, mkApp (f', before), after
in
if dogen then
- let tyf' = Tacmach.New.pf_unsafe_type_of gl f' in
- let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
- Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
+ let sigma', tyf' = Typing.type_of env !sigma f' in
+ sigma := sigma';
+ let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars =
+ Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty) args'
in
let args, refls = List.rev args, List.rev refls in
let vars =
if generalize_vars then
let nogen = Id.Set.add id nogen in
- hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars
+ hyps_of_vars env !sigma hyps nogen vars
else []
in
let body, c' =
@@ -3878,7 +3884,7 @@ let abstract_args gl generalize_vars dep id defined f args =
else None, c'
in
let typ = Tacmach.New.pf_get_hyp_typ id gl in
- let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in
+ let tac = make_abstract_generalize env id typ concl dep ctx body c' eqs args refls in
let tac = Proofview.Unsafe.tclEVARS !sigma <*> tac in
Some (tac, dep, succ (List.length ctx), vars)
else None
@@ -3946,7 +3952,7 @@ let specialize_eqs id =
match EConstr.kind !evars ty with
| Prod (na, t, b) ->
(match EConstr.kind !evars t with
- | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars Coqlib.(lib_ref "core.eq.type") eq ->
+ | App (eq, [| eqty; x; y |]) when isRefX !evars Coqlib.(lib_ref "core.eq.type") eq ->
let c = if noccur_between !evars 1 (List.length ctx) x then y else x in
let pt = mkApp (eq, [| eqty; c; c |]) in
let ind = destInd !evars eq in
@@ -3954,7 +3960,7 @@ let specialize_eqs id =
if unif (push_rel_context ctx env) evars pt t then
aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
else acc, in_eqs, ctx, ty
- | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq ->
+ | App (heq, [| eqty; x; eqty'; y |]) when isRefX !evars (Lazy.force coq_heq_ref) heq ->
let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in
let pt = mkApp (heq, [| eqt; c; eqt; c |]) in
let ind = destInd !evars heq in
@@ -4125,8 +4131,8 @@ let compute_elim_sig sigma ?elimc elimt =
| Some (LocalDef _) -> error_ind_scheme ""
| Some (LocalAssum (_,ind)) ->
let indhd,indargs = decompose_app sigma ind in
- try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) }
- with e when CErrors.noncritical e ->
+ try {!res with indref = Some (fst (destRef sigma indhd)) }
+ with DestKO ->
error "Cannot find the inductive type of the inductive scheme."
let compute_scheme_signature evd scheme names_info ind_type_guess =
@@ -4222,15 +4228,15 @@ let guess_elim isrec dep s hyp0 gl =
let ind = EConstr.of_constr ind in
(sigma, ind)
in
- let elimt = Typing.unsafe_type_of env sigma elimc in
- sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u)
+ let sigma, elimt = Typing.type_of env sigma elimc in
+ sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u)
let given_elim hyp0 (elimc,lbind as e) gl =
let sigma = Tacmach.New.project gl in
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
let ind_type_guess,_ = decompose_app sigma (snd (decompose_prod sigma tmptyp0)) in
- let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
- Tacmach.New.project gl, (e, elimt), ind_type_guess
+ let sigma, elimt = Tacmach.New.pf_type_of gl elimc in
+ sigma, (e, elimt), ind_type_guess
type scheme_signature =
(Id.Set.t * (elim_arg_kind * bool * bool * Id.t) list) array
@@ -4240,33 +4246,32 @@ type eliminator_source =
| ElimOver of bool * Id.t
let find_induction_type isrec elim hyp0 gl =
- let sigma = Tacmach.New.project gl in
- let scheme,elim =
+ let sigma, scheme,elim =
match elim with
| None ->
let sort = Tacticals.New.elimination_sort_of_goal gl in
- let _, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in
+ let sigma, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in
let scheme = compute_elim_sig sigma ~elimc elimt in
(* We drop the scheme waiting to know if it is dependent *)
- scheme, ElimOver (isrec,hyp0)
+ sigma, scheme, ElimOver (isrec,hyp0)
| Some e ->
- let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
+ let sigma, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
let scheme = compute_elim_sig sigma ~elimc elimt in
if Option.is_empty scheme.indarg then error "Cannot find induction type";
- let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in
+ let indsign = compute_scheme_signature sigma scheme hyp0 ind_guess in
let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in
- scheme, ElimUsing (elim,indsign)
+ sigma, scheme, ElimUsing (elim,indsign)
in
match scheme.indref with
| None -> error_ind_scheme ""
- | Some ref -> ref, scheme.nparams, elim
+ | Some ref -> sigma, (ref, scheme.nparams, elim)
let get_elim_signature elim hyp0 gl =
compute_elim_signature (given_elim hyp0 elim gl) hyp0
let is_functional_induction elimc gl =
let sigma = Tacmach.New.project gl in
- let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in
+ let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_get_type_of gl (fst elimc)) in
(* The test is not safe: with non-functional induction on non-standard
induction scheme, this may fail *)
Option.is_empty scheme.indarg
@@ -4380,10 +4385,11 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps =
Proofview.Goal.enter begin fun gl ->
- let elim_info = find_induction_type isrec elim hyp0 gl in
- atomize_param_of_ind_then elim_info hyp0 (fun indvars ->
- apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names
- (fun elim -> induction_tac with_evars [] [hyp0] elim))
+ let sigma, elim_info = find_induction_type isrec elim hyp0 gl in
+ tclEVARSTHEN sigma
+ (atomize_param_of_ind_then elim_info hyp0 (fun indvars ->
+ apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names
+ (fun elim -> induction_tac with_evars [] [hyp0] elim)))
end
let msg_not_right_number_induction_arguments scheme =
@@ -4658,18 +4664,16 @@ let induction_gen_l isrec with_evars elim names lc =
| _ ->
Proofview.Goal.enter begin fun gl ->
- let type_of = Tacmach.New.pf_unsafe_type_of gl in
- let sigma = Tacmach.New.project gl in
- Proofview.tclENV >>= fun env ->
- let x =
- id_of_name_using_hdchar env sigma (type_of c) Anonymous in
-
+ let sigma, t = pf_apply Typing.type_of gl c in
+ let x = id_of_name_using_hdchar (Proofview.Goal.env gl) sigma t Anonymous in
let id = new_fresh_id Id.Set.empty x gl in
let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
let () = newlc:=id::!newlc in
- Tacticals.New.tclTHEN
- (letin_tac None (Name id) c None allHypsAndConcl)
- (atomize_list newl')
+ Tacticals.New.tclTHENLIST [
+ tclEVARS sigma;
+ letin_tac None (Name id) c None allHypsAndConcl;
+ atomize_list newl';
+ ]
end in
Tacticals.New.tclTHENLIST
[
@@ -4765,7 +4769,10 @@ let destruct ev clr c l e =
let elim_scheme_type elim t =
Proofview.Goal.enter begin fun gl ->
- let clause = mk_clenv_type_of gl elim in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma, elimt = Typing.type_of env sigma elim in
+ let clause = mk_clenv_from_env env sigma None (elim,elimt) in
match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with
| Meta mv ->
let clause' =
@@ -4779,7 +4786,9 @@ let elim_scheme_type elim t =
let elim_type t =
Proofview.Goal.enter begin fun gl ->
let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
- let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in
+ let evd, elimc = Tacmach.New.pf_apply find_ind_eliminator gl (fst ind)
+ (Tacticals.New.elimination_sort_of_goal gl)
+ in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t)
end
@@ -4857,7 +4866,8 @@ let prove_symmetry hdcncl eq_kind =
Tacticals.New.onLastHyp simplest_case;
one_constructor 1 NoBindings ])
-let match_with_equation sigma c =
+let match_with_equation c =
+ Proofview.tclEVARMAP >>= fun sigma ->
Proofview.tclENV >>= fun env ->
try
let res = match_with_equation env sigma c in
@@ -4870,9 +4880,8 @@ let symmetry_red allowred =
(* PL: usual symmetry don't perform any reduction when searching
for an equality, but we may need to do some when called back from
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
- let sigma = Tacmach.New.project gl in
let concl = maybe_betadeltaiota_concl allowred gl in
- match_with_equation sigma concl >>= fun with_eqn ->
+ match_with_equation concl >>= fun with_eqn ->
match with_eqn with
| Some eq_data,_,_ ->
Tacticals.New.tclTHEN
@@ -4894,25 +4903,25 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
let symmetry_in id =
Proofview.Goal.enter begin fun gl ->
- let sigma = Tacmach.New.project gl in
- let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
- let sign,t = decompose_prod_assum sigma ctype in
- Proofview.tclORELSE
- begin
- match_with_equation sigma t >>= fun (_,hdcncl,eq) ->
- let symccl =
- match eq with
- | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |])
- | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |])
- | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
- Tacticals.New.tclTHENS (cut (EConstr.it_mkProd_or_LetIn symccl sign))
- [ intro_replacing id;
- Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
- end
- begin function (e, info) -> match e with
- | NoEquationFound -> Hook.get forward_setoid_symmetry_in id
- | e -> Proofview.tclZERO ~info e
- end
+ let sigma, ctype = Tacmach.New.pf_type_of gl (mkVar id) in
+ let sign,t = decompose_prod_assum sigma ctype in
+ tclEVARSTHEN sigma
+ (Proofview.tclORELSE
+ begin
+ match_with_equation t >>= fun (_,hdcncl,eq) ->
+ let symccl =
+ match eq with
+ | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |])
+ | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |])
+ | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
+ Tacticals.New.tclTHENS (cut (EConstr.it_mkProd_or_LetIn symccl sign))
+ [ intro_replacing id;
+ Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
+ end
+ begin function (e, info) -> match e with
+ | NoEquationFound -> Hook.get forward_setoid_symmetry_in id
+ | e -> Proofview.tclZERO ~info e
+ end)
end
let intros_symmetry =
@@ -4939,25 +4948,26 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make ()
(* This is probably not very useful any longer *)
let prove_transitivity hdcncl eq_kind t =
Proofview.Goal.enter begin fun gl ->
- let (eq1,eq2) = match eq_kind with
- | MonomorphicLeibnizEq (c1,c2) ->
- mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |])
- | PolymorphicLeibnizEq (typ,c1,c2) ->
- mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |])
- | HeterogenousEq (typ1,c1,typ2,c2) ->
- let env = Proofview.Goal.env gl in
- let sigma = Tacmach.New.project gl in
- let type_of = Typing.unsafe_type_of env sigma in
- let typt = type_of t in
- (mkApp(hdcncl, [| typ1; c1; typt ;t |]),
- mkApp(hdcncl, [| typt; t; typ2; c2 |]))
- in
- Tacticals.New.tclTHENFIRST (cut eq2)
- (Tacticals.New.tclTHENFIRST (cut eq1)
- (Tacticals.New.tclTHENLIST
- [ Tacticals.New.tclDO 2 intro;
- Tacticals.New.onLastHyp simplest_case;
- assumption ]))
+ let sigma = Tacmach.New.project gl in
+ let sigma, eq1, eq2 = match eq_kind with
+ | MonomorphicLeibnizEq (c1,c2) ->
+ sigma, mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |])
+ | PolymorphicLeibnizEq (typ,c1,c2) ->
+ sigma, mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |])
+ | HeterogenousEq (typ1,c1,typ2,c2) ->
+ let env = Proofview.Goal.env gl in
+ let sigma, typt = Typing.type_of env sigma t in
+ sigma,
+ mkApp(hdcncl, [| typ1; c1; typt ;t |]),
+ mkApp(hdcncl, [| typt; t; typ2; c2 |])
+ in
+ tclEVARSTHEN sigma
+ (Tacticals.New.tclTHENFIRST (cut eq2)
+ (Tacticals.New.tclTHENFIRST (cut eq1)
+ (Tacticals.New.tclTHENLIST
+ [ Tacticals.New.tclDO 2 intro;
+ Tacticals.New.onLastHyp simplest_case;
+ assumption ])))
end
let transitivity_red allowred t =
@@ -4965,9 +4975,8 @@ let transitivity_red allowred t =
(* PL: usual transitivity don't perform any reduction when searching
for an equality, but we may need to do some when called back from
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
- let sigma = Tacmach.New.project gl in
let concl = maybe_betadeltaiota_concl allowred gl in
- match_with_equation sigma concl >>= fun with_eqn ->
+ match_with_equation concl >>= fun with_eqn ->
match with_eqn with
| Some eq_data,_,_ ->
Tacticals.New.tclTHEN
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 17:40:58 +0000