+(* new: demodulation of non_equality terms *)
+let build_newg bag context goal rule expansion =
+ let goalproof,_,_ = goal in
+ let (t,subst,menv,ug,eq_found) = expansion in
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id) =
+ Equality.open_equality equality in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ let newterm, newgoalproof =
+ let bo =
+ Utils.guarded_simpl context
+ (apply_subst subst (CicSubstitution.subst other t))
+ in
+ let bo' = apply_subst subst t in
+ let ty = apply_subst subst ty in
+ let name = Cic.Name "x" in
+ let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, (newgoalproofstep::goalproof)
+ in
+ let newmetasenv = (* Founif.filter subst *) menv in
+ (newgoalproof, newmetasenv, newterm)
+;;
+
+let rec demod bag env table goal =
+ let goalproof,menv,t = goal in
+ let _, context, ugraph = env in
+ let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
+ match res with
+ | Some newt ->
+ let newg =
+ build_newg bag context goal Equality.Demodulation newt
+ in
+ let _,_,newt = newg in
+ if Equality.meta_convertibility t newt then
+ false, goal
+ else
+ true, snd (demod bag env table newg)
+ | None ->
+ false, goal
+;;
+