Almost ready to implement coercion declaration for record fields. But how?

[helm.git] / helm / software / components / tactics / paramodulation / equality.ml

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 5888019e4f78f584c047478a3a13d22b8177561e..2bf3600f289d4de84e76daa71a2f3197bd78c1bb 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -716,7 +716,6 @@ let topological_sort bag l =
   rc
 ;;
   
-
 (* returns the list of ids that should be factorized *)
 let get_duplicate_step_in_wfo bag l p =
   let ol = List.rev l in
@@ -1365,7 +1364,8 @@ let draw_proof bag names goal_proof proof id =
   ignore(Unix.system "gv /tmp/matita_paramod.eps");
 ;;
 
-let saturate_term (id_to_eq, maxmeta) metasenv context term = 
+let saturate_term (id_to_eq, maxmeta) metasenv subst context term = 
+  let maxmeta = max maxmeta (CicMkImplicit.new_meta metasenv subst) in
   let head, metasenv, args, newmeta =
     TermUtil.saturate_term maxmeta metasenv context term 0
   in