- (* we need this cause an equation E like
- F ?x => F ?y
- can add a meta for y in a goal without instantiating it
- P (F true) ----> P (F ?y)
- and this may cause duplicated in metasenvs
- demodulating again with E
- *)
- let bag, new_goals =
- List.fold_right
- (fun g (bag,acc) ->
- let bag, g = Equality.fix_metas_goal bag g in
- bag, g::acc)
- new_goals (bag,[])
+ let nf = if new_goals = [] then goal :: nf else nf in
+ aux steps visited nf bag (new_goals @ rest)
+ in
+ aux steps [] [] bag [goal]
+;;
+
+let combine_demodulation_proofs bag env goal (pl,ml,l) (pr,mr,r) =
+ let proof,m,eq,ty,left,right = open_goal goal in
+ let pl =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
+ | _ -> assert false
+ in
+ rule,pos,id,subst,pred)
+ pl
+ in
+ let pr =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
+ | _ -> assert false