]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/tests/depends
snopshot (working one!)
[helm.git] / matita / tests / depends
index 9ae9703ec904e14c140256156d72404ec4c2057c..200a4088c2e22d117774c0a1fddbbc883f7262ef 100644 (file)
@@ -29,10 +29,13 @@ coercions_open.ma logic/equality.ma nat/nat.ma
 match_inference.ma 
 hard_refine.ma coq.ma
 fix_betareduction.ma coq.ma
+push_pop_status_aux1.ma 
+push_pop_status.ma push_pop_status_aux1.ma
 decl.ma nat/orders.ma nat/times.ma
 pullback.ma 
 mysql_escaping.ma 
 rewrite.ma coq.ma
+push_pop_status_aux2.ma 
 injection.ma coq.ma
 contradiction.ma coq.ma
 fold.ma coq.ma