aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/g_auto.mlg11
-rw-r--r--plugins/ltac/g_class.mlg2
-rw-r--r--plugins/ltac/g_tactic.mlg11
-rw-r--r--plugins/ltac/pptactic.ml5
-rw-r--r--plugins/ltac/rewrite.ml74
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacexpr.ml3
-rw-r--r--plugins/ltac/tacexpr.mli3
-rw-r--r--plugins/ltac/tacintern.ml8
-rw-r--r--plugins/ltac/tacinterp.ml8
-rw-r--r--plugins/ltac/tacsubst.ml10
-rw-r--r--plugins/ltac/tauto.ml18
12 files changed, 92 insertions, 63 deletions
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 523c7c8305..e59076bd63 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -182,9 +182,18 @@ TACTIC EXTEND unify
}
END
+{
+let deprecated_convert_concl_no_check =
+ CWarnings.create
+ ~name:"convert_concl_no_check" ~category:"deprecated"
+ (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.")
+}
TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast }
+| ["convert_concl_no_check" constr(x) ] -> {
+ deprecated_convert_concl_no_check ();
+ Tactics.convert_concl ~check:false x DEFAULTcast
+ }
END
{
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 3f2fabeeee..049a699cbd 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -84,7 +84,7 @@ TACTIC EXTEND typeclasses_eauto
| [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d l }
| [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
- typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] }
+ typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] }
END
TACTIC EXTEND head_of_constr
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 7bf705ffeb..c23240b782 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -72,7 +72,7 @@ let test_lpar_idnum_coloneq =
match stream_nth 0 strm with
| KEYWORD "(" ->
(match stream_nth 1 strm with
- | IDENT _ | INT _ ->
+ | IDENT _ | NUMERAL _ ->
(match stream_nth 2 strm with
| KEYWORD ":=" -> ()
| _ -> err ())
@@ -147,7 +147,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
end
| _ -> ElimOnConstr clbind
-let mkNumeral n = Numeral (string_of_int (abs n), 0<=n)
+let mkNumeral n =
+ Numeral ((if 0<=n then SPlus else SMinus),NumTok.int (string_of_int (abs n)))
let mkTacCase with_evar = function
| [(clear,ElimOnConstr cl),(None,None),None],None ->
@@ -702,7 +703,11 @@ GRAMMAR EXTEND Gram
| IDENT "change"; c = conversion; cl = clause_dft_concl ->
{ let (oc, c) = c in
let p,cl = merge_occurrences loc cl oc in
- TacAtom (CAst.make ~loc @@ TacChange (p,c,cl)) }
+ TacAtom (CAst.make ~loc @@ TacChange (true,p,c,cl)) }
+ | IDENT "change_no_check"; c = conversion; cl = clause_dft_concl ->
+ { let (oc, c) = c in
+ let p,cl = merge_occurrences loc cl oc in
+ TacAtom (CAst.make ~loc @@ TacChange (false,p,c,cl)) }
] ]
;
END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 80070a7493..79f0f521cc 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -833,9 +833,10 @@ let pr_goal_selector ~toplevel s =
pr_red_expr r
++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
)
- | TacChange (op,c,h) ->
+ | TacChange (check,op,c,h) ->
+ let name = if check then "change_no_check" else "change" in
hov 1 (
- primitive "change" ++ brk (1,1)
+ primitive name ++ brk (1,1)
++ (
match op with
None ->
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 75565c1a34..a68efa4713 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -119,7 +119,7 @@ let app_poly_check env evars f args =
(evars, cstrs), t
let app_poly_nocheck env evars f args =
- let evars, fc = f evars in
+ let evars, fc = f evars in
evars, mkApp (fc, args)
let app_poly_sort b =
@@ -175,25 +175,29 @@ end) = struct
let rewrite_relation_class = find_global relation_classes "RewriteRelation"
- let proper_class = lazy (class_info (find_reference morphisms "Proper"))
- let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy"))
-
- let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
-
- let proper_type =
- let l = lazy (Lazy.force proper_class).cl_impl in
- fun (evd,cstrs) ->
- let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
- (evd, cstrs), c
-
- let proper_proxy_type =
- let l = lazy (Lazy.force proper_proxy_class).cl_impl in
- fun (evd,cstrs) ->
- let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
- (evd, cstrs), c
+ let proper_class =
+ let r = lazy (find_reference morphisms "Proper") in
+ fun env sigma -> class_info env sigma (Lazy.force r)
+
+ let proper_proxy_class =
+ let r = lazy (find_reference morphisms "ProperProxy") in
+ fun env sigma -> class_info env sigma (Lazy.force r)
+
+ let proper_proj env sigma =
+ mkConst (Option.get (pi3 (List.hd (proper_class env sigma).cl_projs)))
+
+ let proper_type env (sigma,cstrs) =
+ let l = (proper_class env sigma).cl_impl in
+ let (sigma, c) = Evarutil.new_global sigma l in
+ (sigma, cstrs), c
+
+ let proper_proxy_type env (sigma,cstrs) =
+ let l = (proper_proxy_class env sigma).cl_impl in
+ let (sigma, c) = Evarutil.new_global sigma l in
+ (sigma, cstrs), c
let proper_proof env evars carrier relation x =
- let evars, goal = app_poly env evars proper_proxy_type [| carrier ; relation; x |] in
+ let evars, goal = app_poly env evars (proper_proxy_type env) [| carrier ; relation; x |] in
new_cstr_evar evars env goal
let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
@@ -800,7 +804,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
in
(* Actual signature found *)
let cl_args = [| appmtype' ; signature ; appm |] in
- let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type else TypeGlobal.proper_type)
+ let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type env else TypeGlobal.proper_type env)
cl_args in
let env' =
let dosub, appsub =
@@ -1310,8 +1314,8 @@ module Strategies =
in
let evars, proof =
let proxy =
- if prop then PropGlobal.proper_proxy_type
- else TypeGlobal.proper_proxy_type
+ if prop then PropGlobal.proper_proxy_type env
+ else TypeGlobal.proper_proxy_type env
in
let evars, mty = app_poly_sort prop env evars proxy [| ty ; rel; t |] in
new_cstr_evar evars env mty
@@ -1570,8 +1574,8 @@ let newfail n s =
let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let open Proofview.Notations in
(* For compatibility *)
- let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
- let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in
+ let beta = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in
+ let beta_hyp id = Tactics.reduct_in_hyp ~check:false ~reorder:false Reductionops.nf_betaiota (id, InHyp) in
let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
@@ -1592,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
| Some id, None ->
Proofview.Unsafe.tclEVARS undef <*>
- convert_hyp_no_check (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
+ convert_hyp ~check:false ~reorder:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
beta_hyp id
| None, Some p ->
Proofview.Unsafe.tclEVARS undef <*>
@@ -1606,7 +1610,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
end
| None, None ->
Proofview.Unsafe.tclEVARS undef <*>
- convert_concl_no_check newt DEFAULTcast
+ convert_concl ~check:false newt DEFAULTcast
in
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
@@ -1854,12 +1858,12 @@ let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
-let proper_projection sigma r ty =
+let proper_projection env sigma r ty =
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
let ctx, inst = decompose_prod_assum sigma ty in
let mor, args = destApp sigma inst in
let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
- let app = mkApp (Lazy.force PropGlobal.proper_proj,
+ let app = mkApp (PropGlobal.proper_proj env sigma,
Array.append args [| instarg |]) in
it_mkLambda_or_LetIn app ctx
@@ -1869,7 +1873,7 @@ let declare_projection n instance_id r =
let sigma = Evd.from_env env in
let sigma,c = Evd.fresh_global env sigma r in
let ty = Retyping.get_type_of env sigma c in
- let term = proper_projection sigma c ty in
+ let term = proper_projection env sigma c ty in
let sigma, typ = Typing.type_of env sigma term in
let ctx, typ = decompose_prod_assum sigma typ in
let typ =
@@ -1924,7 +1928,7 @@ let build_morphism_signature env sigma m =
rel)
cstrs
in
- let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
+ let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in
let evd = solve_constraints env !evd in
let evd = Evd.minimize_universes evd in
let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
@@ -1938,9 +1942,9 @@ let default_morphism sign m =
let evars, _, sign, cstrs =
PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
in
- let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in
+ let evars, morph = app_poly_check env evars (PropGlobal.proper_type env) [| t; sign; m |] in
let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
- mor, proper_projection sigma mor morph
+ mor, proper_projection env sigma mor morph
let warn_add_setoid_deprecated =
CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
@@ -1984,8 +1988,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
(None,(instance,uctx),None),
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
- add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
+ add_instance (Classes.mk_instance
+ (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
declare_projection n instance_id (ConstRef cst);
pstate
else
@@ -1995,8 +1999,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
let hook _ _ _ = function
| Globnames.ConstRef cst ->
- add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
+ add_instance (Classes.mk_instance
+ (PropGlobal.proper_class env evd) Hints.empty_hint_info
atts.global (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
| _ -> assert false
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index b770b97384..814be64f81 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -48,7 +48,7 @@ let atactic n =
else Aentryl (Pltac.tactic_expr, string_of_int n)
type entry_name = EntryName :
- 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
+ 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name
(** Quite ad-hoc *)
let get_tacentry n m =
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 30e316b36d..0eb7726a18 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -34,6 +34,7 @@ type rec_flag = bool (* true = recursive false = not recursive *)
type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+type check_flag = bool (* true = check false = do not check *)
type ('c,'d,'id) inversion_strength =
| NonDepInversion of
@@ -125,7 +126,7 @@ type 'a gen_atomic_tactic_expr =
(* Conversion *)
| TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
- | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+ | TacChange of check_flag * 'pat option * 'dtrm * 'nam clause_expr
(* Equality and inversion *)
| TacRewrite of evars_flag *
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 8b6b14322b..fd303f5d94 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -34,6 +34,7 @@ type rec_flag = bool (* true = recursive false = not recursive *)
type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+type check_flag = bool (* true = check false = do not check *)
type ('c,'d,'id) inversion_strength =
| NonDepInversion of
@@ -124,7 +125,7 @@ type 'a gen_atomic_tactic_expr =
(* Conversion *)
| TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
- | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+ | TacChange of check_flag * 'pat option * 'dtrm * 'nam clause_expr
(* Equality and inversion *)
| TacRewrite of evars_flag *
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 543d4de0fe..c1f7fab123 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -551,7 +551,7 @@ let rec intern_atomic lf ist x =
| TacReduce (r,cl) ->
dump_glob_red_expr r;
TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
- | TacChange (None,c,cl) ->
+ | TacChange (check,None,c,cl) ->
let is_onhyps = match cl.onhyps with
| None | Some [] -> true
| _ -> false
@@ -560,17 +560,17 @@ let rec intern_atomic lf ist x =
| AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
| _ -> false
in
- TacChange (None,
+ TacChange (check,None,
(if is_onhyps && is_onconcl
then intern_type ist c else intern_constr ist c),
clause_app (intern_hyp_location ist) cl)
- | TacChange (Some p,c,cl) ->
+ | TacChange (check,Some p,c,cl) ->
let { ltacvars } = ist in
let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in
let fold accu x = Id.Set.add x accu in
let ltacvars = List.fold_left fold ltacvars metas in
let ist' = { ist with ltacvars } in
- TacChange (Some pat,intern_constr ist' c,
+ TacChange (check,Some pat,intern_constr ist' c,
clause_app (intern_hyp_location ist) cl)
(* Equality and inversion *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 4398fb14ab..800be2565d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1770,7 +1770,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))
end
- | TacChange (None,c,cl) ->
+ | TacChange (check,None,c,cl) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
Proofview.Goal.enter begin fun gl ->
@@ -1792,10 +1792,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
then interp_type ist env sigma c
else interp_constr ist env sigma c
in
- Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
+ Tactics.change ~check None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
end
end
- | TacChange (Some op,c,cl) ->
+ | TacChange (check,Some op,c,cl) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
Proofview.Goal.enter begin fun gl ->
@@ -1815,7 +1815,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
with e when to_catch e (* Hack *) ->
user_err (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
in
- Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
+ Tactics.change ~check (Some op) c_interp (interp_clause ist env sigma cl)
end
end
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index caaa547a07..a3eeca2267 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -30,7 +30,7 @@ let subst_quantified_hypothesis _ x = x
let subst_declared_or_quantified_hypothesis _ x = x
let subst_glob_constr_and_expr subst (c, e) =
- (Detyping.subst_glob_constr subst c, e)
+ (Detyping.subst_glob_constr (Global.env()) subst c, e)
let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
@@ -99,7 +99,9 @@ let subst_evaluable subst =
let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
let subst_glob_constr_or_pattern subst (bvars,c,p) =
- (bvars,subst_glob_constr subst c,subst_pattern subst p)
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ (bvars,subst_glob_constr subst c,subst_pattern env sigma subst p)
let subst_redexp subst =
Redops.map_red_expr_gen
@@ -156,8 +158,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Conversion *)
| TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
- | TacChange (op,c,cl) ->
- TacChange (Option.map (subst_glob_constr_or_pattern subst) op,
+ | TacChange (check,op,c,cl) ->
+ TacChange (check,Option.map (subst_glob_constr_or_pattern subst) op,
subst_glob_constr subst c, cl)
(* Equality and inversion *)
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 4c65445b89..d1951cc18d 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -98,16 +98,18 @@ let split = Tactics.split_with_bindings false [Tactypes.NoBindings]
(** Test *)
let is_empty _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
- if is_empty_type sigma (assoc_var "X1" ist) then idtac else fail
+ if is_empty_type genv sigma (assoc_var "X1" ist) then idtac else fail
(* Strictly speaking, this exceeds the propositional fragment as it
matches also equality types (and solves them if a reflexivity) *)
let is_unit_or_eq _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in
- if test sigma (assoc_var "X1" ist) then idtac else fail
+ if test genv sigma (assoc_var "X1" ist) then idtac else fail
let bugged_is_binary sigma t =
isApp sigma t &&
@@ -121,23 +123,25 @@ let bugged_is_binary sigma t =
(** Dealing with conjunction *)
let is_conj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let ind = assoc_var "X1" ist in
if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma ind) &&
- is_conjunction sigma
+ is_conjunction genv sigma
~strict:flags.strict_in_hyp_and_ccl
~onlybinary:flags.binary_mode ind
then idtac
else fail
let flatten_contravariant_conj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
let hyp = assoc_var "id" ist in
- match match_with_conjunction sigma
+ match match_with_conjunction genv sigma
~strict:flags.strict_in_contravariant_hyp
~onlybinary:flags.binary_mode typ
with
@@ -151,23 +155,25 @@ let flatten_contravariant_conj _ ist =
(** Dealing with disjunction *)
let is_disj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let t = assoc_var "X1" ist in
if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma t) &&
- is_disjunction sigma
+ is_disjunction genv sigma
~strict:flags.strict_in_hyp_and_ccl
~onlybinary:flags.binary_mode t
then idtac
else fail
let flatten_contravariant_disj _ ist =
+ Proofview.tclENV >>= fun genv ->
Proofview.tclEVARMAP >>= fun sigma ->
let flags = assoc_flags ist in
let typ = assoc_var "X1" ist in
let c = assoc_var "X2" ist in
let hyp = assoc_var "id" ist in
- match match_with_disjunction sigma
+ match match_with_disjunction genv sigma
~strict:flags.strict_in_contravariant_hyp
~onlybinary:flags.binary_mode
typ with
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:21:54 +0000