aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/formula.ml2
-rw-r--r--plugins/firstorder/formula.mli8
-rw-r--r--plugins/firstorder/g_ground.mlg (renamed from plugins/firstorder/g_ground.ml4)71
-rw-r--r--plugins/firstorder/ground.ml16
-rw-r--r--plugins/firstorder/instances.ml9
-rw-r--r--plugins/firstorder/instances.mli4
-rw-r--r--plugins/firstorder/plugin_base.dune5
-rw-r--r--plugins/firstorder/rules.ml26
-rw-r--r--plugins/firstorder/rules.mli11
-rw-r--r--plugins/firstorder/sequent.ml34
-rw-r--r--plugins/firstorder/sequent.mli22
-rw-r--r--plugins/firstorder/unify.ml6
12 files changed, 97 insertions, 117 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 047fc9fbfd..a60a966cec 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -211,7 +211,7 @@ type left_pattern=
| Lexists of pinductive
| LA of constr*left_arrow_pattern
-type t={id:global_reference;
+type t={id:GlobRef.t;
constr:constr;
pat:(left_pattern,right_pattern) sum;
atoms:atoms}
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 2962d9230d..e2c6f1c4b1 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -8,9 +8,9 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+open Names
open Constr
open EConstr
-open Globnames
val qflag : bool ref
@@ -35,7 +35,7 @@ type atoms = {positive:constr list;negative:constr list}
type side = Hyp | Concl | Hint
-val dummy_id: global_reference
+val dummy_id: GlobRef.t
val build_atoms : Environ.env -> Evd.evar_map -> counter ->
side -> constr -> bool * atoms
@@ -65,13 +65,13 @@ type left_pattern=
| Lexists of pinductive
| LA of constr*left_arrow_pattern
-type t={id: global_reference;
+type t={id: GlobRef.t;
constr: constr;
pat: (left_pattern,right_pattern) sum;
atoms: atoms}
(*exception Is_atom of constr*)
-val build_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> types ->
+val build_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> types ->
counter -> (t,types) sum
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.mlg
index 30deb6f49a..a212d13453 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.mlg
@@ -8,6 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
open Ltac_plugin
open Formula
@@ -17,15 +18,19 @@ open Goptions
open Tacmach.New
open Tacticals.New
open Tacinterp
-open Libnames
open Stdarg
open Tacarg
+open Attributes
open Pcoq.Prim
+}
+
DECLARE PLUGIN "ground_plugin"
(* declaring search depth as a global option *)
+{
+
let ground_depth=ref 3
let _=
@@ -61,28 +66,28 @@ let default_intuition_tac =
let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
Tacenv.register_ml_tactic name [| tac |];
- Tacexpr.TacML (Loc.tag (entry, []))
+ Tacexpr.TacML (CAst.make (entry, []))
let (set_default_solver, default_solver, print_default_solver) =
Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
-VERNAC COMMAND FUNCTIONAL EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
-| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
- fun ~atts ~st -> let open Vernacinterp in
+}
+
+VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
+| #[ locality; ] [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
set_default_solver
- (Locality.make_section_locality atts.locality)
- (Tacintern.glob_tactic t);
- st
- ]
+ (Locality.make_section_locality locality)
+ (Tacintern.glob_tactic t)
+ }
END
VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
-| [ "Print" "Firstorder" "Solver" ] -> [
+| [ "Print" "Firstorder" "Solver" ] -> {
Feedback.msg_info
- (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
+ (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) }
END
-let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
+{
let gen_ground_tac flag taco ids bases =
let backup= !qflag in
@@ -110,11 +115,11 @@ let gen_ground_tac flag taco ids bases =
(* special for compatibility with Intuition
-let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
+let constant str = Coqlib.get_constr str
let defined_connectives=lazy
- [[],EvalConstRef (destConst (constant "not"));
- [],EvalConstRef (destConst (constant "iff"))]
+ [[],EvalConstRef (destConst (constant "core.not.type"));
+ [],EvalConstRef (destConst (constant "core.iff.type"))]
let normalize_evaluables=
onAllHypsAndConcl
@@ -124,10 +129,9 @@ let normalize_evaluables=
unfold_in_hyp (Lazy.force defined_connectives)
(Tacexpr.InHypType id)) *)
-open Genarg
open Ppconstr
open Printer
-let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference
+let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid
let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
@@ -135,34 +139,33 @@ let warn_deprecated_syntax =
CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
(fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator")
+}
ARGUMENT EXTEND firstorder_using
- TYPED AS reference_list
- PRINTED BY pr_firstorder_using_typed
- RAW_TYPED AS reference_list
- RAW_PRINTED BY pr_firstorder_using_raw
- GLOB_TYPED AS reference_list
- GLOB_PRINTED BY pr_firstorder_using_glob
-| [ "using" reference(a) ] -> [ [a] ]
-| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
-| [ "using" reference(a) reference(b) reference_list(l) ] -> [
+ TYPED AS reference list
+ PRINTED BY { pr_firstorder_using_typed }
+ RAW_PRINTED BY { pr_firstorder_using_raw }
+ GLOB_PRINTED BY { pr_firstorder_using_glob }
+| [ "using" reference(a) ] -> { [a] }
+| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> { a::l }
+| [ "using" reference(a) reference(b) reference_list(l) ] -> {
warn_deprecated_syntax ();
a::b::l
- ]
-| [ ] -> [ [] ]
+ }
+| [ ] -> { [] }
END
TACTIC EXTEND firstorder
- [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
- [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] ]
+| [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
+ { gen_ground_tac true (Option.map (tactic_of_value ist) t) l [] }
| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
- [ gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l ]
+ { gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l }
| [ "firstorder" tactic_opt(t) firstorder_using(l)
"with" ne_preident_list(l') ] ->
- [ gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' ]
+ { gen_ground_tac true (Option.map (tactic_of_value ist) t) l l' }
END
TACTIC EXTEND gintuition
- [ "gintuition" tactic_opt(t) ] ->
- [ gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] ]
+| [ "gintuition" tactic_opt(t) ] ->
+ { gen_ground_tac false (Option.map (tactic_of_value ist) t) [] [] }
END
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 4e3ba57308..6a80525200 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -13,23 +13,21 @@ open Formula
open Sequent
open Rules
open Instances
-open Constr
open Tacmach.New
open Tacticals.New
+open Globnames
let update_flags ()=
- let predref=ref Names.Cpred.empty in
- let f coe=
- try
- let kn= fst (destConst (Classops.get_coercion_value coe)) in
- predref:=Names.Cpred.add kn !predref
- with DestKO -> ()
+ let open TransparentState in
+ let f accu coe = match coe.Classops.coe_value with
+ | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
+ | _ -> accu
in
- List.iter f (Classops.coercions ());
+ let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in
red_flags:=
CClosure.RedFlags.red_add_transparent
CClosure.betaiotazeta
- (Names.Id.Pred.full,Names.Cpred.complement !predref)
+ flags
let ground_tac solver startseq =
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index e8c0b927dc..286021d68e 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -22,7 +22,6 @@ open Reductionops
open Formula
open Sequent
open Names
-open Misctypes
open Context.Rel.Declaration
let compare_instance inst1 inst2=
@@ -39,11 +38,11 @@ let compare_gr id1 id2 =
if id1==id2 then 0 else
if id1==dummy_id then 1
else if id2==dummy_id then -1
- else Globnames.RefOrdered.compare id1 id2
+ else GlobRef.Ordered.compare id1 id2
module OrderedInstance=
struct
- type t=instance * Globnames.global_reference
+ type t=instance * GlobRef.t
let compare (inst1,id1) (inst2,id2)=
(compare_instance =? compare_gr) inst2 inst1 id2 id1
(* we want a __decreasing__ total order *)
@@ -184,12 +183,12 @@ let right_instance_tac inst continue seq=
[introf;
Proofview.Goal.enter begin fun gl ->
let id0 = List.nth (pf_ids_of_hyps gl) 0 in
- split (ImplicitBindings [mkVar id0])
+ split (Tactypes.ImplicitBindings [mkVar id0])
end;
tclSOLVE [wrap 0 true continue (deepen seq)]];
tclTRY assumption]
| Real ((0,t),_) ->
- (tclTHEN (split (ImplicitBindings [t]))
+ (tclTHEN (split (Tactypes.ImplicitBindings [t]))
(tclSOLVE [wrap 0 true continue (deepen seq)]))
| Real ((m,t),_) ->
tclFAIL 0 (Pp.str "not implemented ... yet")
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 61786ffdc9..9f9ade3aab 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -8,13 +8,13 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Globnames
+open Names
open Rules
val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t
val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t ->
- (Unify.instance * global_reference) list
+ (Unify.instance * GlobRef.t) list
val quantified_tac : Formula.t list -> seqtac with_backtracking
diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/plugin_base.dune
new file mode 100644
index 0000000000..d88daa23fc
--- /dev/null
+++ b/plugins/firstorder/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name ground_plugin)
+ (public_name coq.plugins.firstorder)
+ (synopsis "Coq's first order logic solver plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index cfcd656191..832a98b7f8 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -21,7 +21,6 @@ open Termops
open Formula
open Sequent
open Globnames
-open Locus
module NamedDecl = Context.Named.Declaration
@@ -29,12 +28,12 @@ type tactic = unit Proofview.tactic
type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
-type lseqtac= global_reference -> seqtac
+type lseqtac= GlobRef.t -> seqtac
type 'a with_backtracking = tactic -> 'a
let wrap n b continue seq =
- Proofview.Goal.nf_enter begin fun gls ->
+ Proofview.Goal.enter begin fun gls ->
Control.check_for_interrupt ();
let nc = Proofview.Goal.hyps gls in
let env=pf_env gls in
@@ -56,10 +55,6 @@ let wrap n b continue seq =
continue seq2
end
-let basename_of_global=function
- VarRef id->id
- | _->assert false
-
let clear_global=function
VarRef id-> clear [id]
| _->tclIDTAC
@@ -230,20 +225,3 @@ let ll_forall_tac prod backtrack id continue seq=
backtrack
(* rules for instantiation with unification moved to instances.ml *)
-
-(* special for compatibility with old Intuition *)
-
-let constant str = Universes.constr_of_global
- @@ Coqlib.coq_reference "User" ["Init";"Logic"] str
-
-let defined_connectives=lazy
- [AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "not")));
- AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "iff")))]
-
-let normalize_evaluables=
- Proofview.Goal.enter begin fun gl ->
- unfold_in_concl (Lazy.force defined_connectives) <*>
- tclMAP
- (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
- (pf_ids_of_hyps gl)
- end
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 859388b303..97bc992b26 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -11,21 +11,18 @@
open Names
open Constr
open EConstr
-open Globnames
type tactic = unit Proofview.tactic
type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
-type lseqtac= global_reference -> seqtac
+type lseqtac= GlobRef.t -> seqtac
type 'a with_backtracking = tactic -> 'a
val wrap : int -> bool -> seqtac
-val basename_of_global: global_reference -> Id.t
-
-val clear_global: global_reference -> tactic
+val clear_global: GlobRef.t -> tactic
val axiom_tac : constr -> Sequent.t -> tactic
@@ -41,7 +38,7 @@ val left_and_tac : pinductive -> lseqtac with_backtracking
val left_or_tac : pinductive -> lseqtac with_backtracking
-val left_false_tac : global_reference -> tactic
+val left_false_tac : GlobRef.t -> tactic
val ll_ind_tac : pinductive -> constr list -> lseqtac with_backtracking
@@ -52,5 +49,3 @@ val forall_tac : seqtac with_backtracking
val left_exists_tac : pinductive -> lseqtac with_backtracking
val ll_forall_tac : types -> lseqtac with_backtracking
-
-val normalize_evaluables : tactic
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 2859917978..5958fe8203 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -8,13 +8,13 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open EConstr
-open CErrors
open Util
+open Pp
+open CErrors
+open Names
+open EConstr
open Formula
open Unify
-open Globnames
-open Pp
let newcnt ()=
let cnt=ref (-1) in
@@ -56,13 +56,13 @@ struct
(priority e1.pat) - (priority e2.pat)
end
-type h_item = global_reference * (int*Constr.t) option
+type h_item = GlobRef.t * (int*Constr.t) option
module Hitem=
struct
type t = h_item
let compare (id1,co1) (id2,co2)=
- let c = Globnames.RefOrdered.compare id1 id2 in
+ let c = GlobRef.Ordered.compare id1 id2 in
if c = 0 then
let cmp (i1, c1) (i2, c2) =
let c = Int.compare i1 i2 in
@@ -77,17 +77,17 @@ module CM=Map.Make(Constr)
module History=Set.Make(Hitem)
let cm_add sigma typ nam cm=
- let typ = EConstr.to_constr sigma typ in
+ let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
try
let l=CM.find typ cm in CM.add typ (nam::l) cm
with
Not_found->CM.add typ [nam] cm
let cm_remove sigma typ nam cm=
- let typ = EConstr.to_constr sigma typ in
+ let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
try
let l=CM.find typ cm in
- let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
+ let l0=List.filter (fun id-> not (GlobRef.equal id nam)) l in
match l0 with
[]->CM.remove typ cm
| _ ->CM.add typ l0 cm
@@ -97,7 +97,7 @@ module HP=Heap.Functional(OrderedFormula)
type t=
{redexes:HP.t;
- context:(global_reference list) CM.t;
+ context:(GlobRef.t list) CM.t;
latoms:constr list;
gl:types;
glatom:constr option;
@@ -117,7 +117,7 @@ let lookup sigma item seq=
let p (id2,o)=
match o with
None -> false
- | Some (m2, t2)-> Globnames.eq_gr id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
+ | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
History.exists p seq.history
let add_formula env sigma side nam t seq =
@@ -152,7 +152,7 @@ let re_add_formula_list sigma lf seq=
redexes=List.fold_right HP.add lf seq.redexes;
context=List.fold_right do_one lf seq.context}
-let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context)
+let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) seq.context)
(*let rev_left seq=
try
@@ -187,9 +187,9 @@ let empty_seq depth=
let expand_constructor_hints =
List.map_append (function
- | IndRef ind ->
+ | GlobRef.IndRef ind ->
List.init (Inductiveops.nconstructors ind)
- (fun i -> ConstructRef (ind,i+1))
+ (fun i -> GlobRef.ConstructRef (ind,i+1))
| gr ->
[gr])
@@ -197,7 +197,7 @@ let extend_with_ref_list env sigma l seq =
let l = expand_constructor_hints l in
let f gr (seq, sigma) =
let sigma, c = Evd.fresh_global env sigma gr in
- let sigma, typ= Typing.type_of env sigma (EConstr.of_constr c) in
+ let sigma, typ= Typing.type_of env sigma c in
(add_formula env sigma Hyp gr typ seq, sigma) in
List.fold_right f l (seq, sigma)
@@ -229,7 +229,9 @@ let extend_with_auto_hints env sigma l seq =
let print_cmap map=
let print_entry c l s=
- let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty (EConstr.of_constr c) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in
str "| " ++
prlist Printer.pr_global l ++
str " : " ++
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index c4ed3e21fd..709b278ec4 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -8,26 +8,26 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+open Names
open EConstr
open Formula
-open Globnames
module CM: CSig.MapS with type key=Constr.t
-type h_item = global_reference * (int*Constr.t) option
+type h_item = GlobRef.t * (int*Constr.t) option
module History: Set.S with type elt = h_item
-val cm_add : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t ->
- global_reference list CM.t
+val cm_add : Evd.evar_map -> constr -> GlobRef.t -> GlobRef.t list CM.t ->
+ GlobRef.t list CM.t
-val cm_remove : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t ->
- global_reference list CM.t
+val cm_remove : Evd.evar_map -> constr -> GlobRef.t -> GlobRef.t list CM.t ->
+ GlobRef.t list CM.t
module HP: Heap.S with type elt=Formula.t
type t = {redexes:HP.t;
- context: global_reference list CM.t;
+ context: GlobRef.t list CM.t;
latoms:constr list;
gl:types;
glatom:constr option;
@@ -41,20 +41,20 @@ val record: h_item -> t -> t
val lookup: Evd.evar_map -> h_item -> t -> bool
-val add_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> constr -> t -> t
+val add_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> constr -> t -> t
val re_add_formula_list : Evd.evar_map -> Formula.t list -> t -> t
-val find_left : Evd.evar_map -> constr -> t -> global_reference
+val find_left : Evd.evar_map -> constr -> t -> GlobRef.t
val take_formula : Evd.evar_map -> t -> Formula.t * t
val empty_seq : int -> t
-val extend_with_ref_list : Environ.env -> Evd.evar_map -> global_reference list ->
+val extend_with_ref_list : Environ.env -> Evd.evar_map -> GlobRef.t list ->
t -> t * Evd.evar_map
val extend_with_auto_hints : Environ.env -> Evd.evar_map -> Hints.hint_db_name list ->
t -> t * Evd.evar_map
-val print_cmap: global_reference list CM.t -> Pp.t
+val print_cmap: GlobRef.t list CM.t -> Pp.t
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index b869c04a21..d63fe9d799 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -9,7 +9,7 @@
(************************************************************************)
open Util
-open Term
+open Constr
open EConstr
open Vars
open Termops
@@ -56,12 +56,12 @@ let unif evd t1 t2=
| Meta i,_ ->
let t=subst_meta !sigma nt2 in
if Int.Set.is_empty (free_rels evd t) &&
- not (dependent evd (EConstr.mkMeta i) t) then
+ not (occur_metavariable evd i t) then
bind i t else raise (UFAIL(nt1,nt2))
| _,Meta i ->
let t=subst_meta !sigma nt1 in
if Int.Set.is_empty (free_rels evd t) &&
- not (dependent evd (EConstr.mkMeta i) t) then
+ not (occur_metavariable evd i t) then
bind i t else raise (UFAIL(nt1,nt2))
| Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige
| _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 17:25:08 +0000