let compose_contexts ctx1 ctx2 =
ProofEngineReduction.replace_lifting
- ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
+ ~equality:(fun _ ->(=)) ~context:[] ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
;;
let put_in_ctx ctx t =
ProofEngineReduction.replace_lifting
- ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
+ ~equality:(fun _ -> (=)) ~context:[] ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
;;
let mk_eq uri ty l r =
let p = CicSubstitution.lift (lift_no-1) p in
let p =
ProofEngineReduction.replace_lifting
- ~equality:(fun t1 t2 ->
+ ~equality:(fun _ t1 t2 ->
match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false)
+ ~context:[]
~what ~with_what ~where:p
in
let ty_of_m _ = Cic.Implicit (Some `Type) in