From 1ae74bfd16f00bea0de14299cace8b638f768a70 Mon Sep 17 00:00:00 2001
From: Frédéric Besson <frederic.besson@inria.fr>
Date: Thu, 1 Sep 2016 16:21:11 +0200
Subject: Fixed Bug #5003 : more careful generalisation of dependent terms.

---
 plugins/micromega/coq_micromega.ml | 35 ++++++++++++++++++++++++++++++++---
 1 file changed, 32 insertions(+), 3 deletions(-)

(limited to 'plugins/micromega/coq_micromega.ml')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index edcb00b90..42ea8c459 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1437,7 +1437,36 @@ let rcst_domain_spec  = lazy {
 
 open Proofview.Notations
 
- 
+(** Naive topological sort of constr according to the subterm-ordering *)
+
+(* An element is minimal x is minimal w.r.t y if 
+   x <= y or (x and y are incomparable) *)
+
+let is_min le x y =
+  if le x y then true
+  else    if le y x then false else true
+
+let is_minimal le l c = List.for_all (is_min le c) l
+    
+let find_rem p l =
+  let rec xfind_rem  acc l =
+    match l with
+    | [] -> (None, acc)
+    | x :: l -> if p x then (Some x, acc @ l)
+      else xfind_rem (x::acc) l in
+  xfind_rem [] l
+
+let find_minimal le l = find_rem (is_minimal le l) l
+  
+let rec mk_topo_order le l =
+  match find_minimal le l with
+  | (None , _) -> []
+  | (Some v,l') -> v ::  (mk_topo_order le l')
+
+    
+let topo_sort_constr l = mk_topo_order Termops.dependent l
+
+
 (**
   * Instanciate the current Coq goal with a Micromega formula, a varmap, and a
   * witness.
@@ -1464,7 +1493,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
       ]
       (Tacmach.pf_concl gl))
    ;
-   Tactics.generalize env ;
+      Tactics.generalize (topo_sort_constr env) ;
    Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
   ] 
   end }
@@ -1774,7 +1803,7 @@ let micromega_order_changer cert env ff  =
          ("__wit", cert, cert_typ)
         ]
         (Tacmach.pf_concl gl)));
-      Tactics.generalize env ;
+      Tactics.generalize (topo_sort_constr env) ;
       Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
      ]
   end }
-- 
cgit v1.2.3