Ground update + Linear removal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4654 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 70 deletions

diff --git a/contrib/linear/graph.ml b/contrib/linear/graph.ml
deleted file mode 100755
index 94ddcbd97..000000000
--- a/contrib/linear/graph.ml
+++ /dev/null
@@ -1,70 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-(* Given a DIRECTED graph G represented by a list of 
-   (x , [neighbours of x])
-   then (have_cycle G) returns true if G has a nontrivial cycle.
-   Remark : G is not necessarly connected. *******)
-  
-type mark = NotMarked | OnThePath | AlreadyVisited;;
-
-let df_cycle v marks g =
-  let rec df_cycle_rec x = 
-    (List.assoc x marks) := OnThePath;
-       let nx  = List.assoc x g
-    in let nb_marks = 
-           List.fold_left (fun s x -> if !(List.assoc x marks)=OnThePath 
-      	       	       	       then s+1 else s) 0 nx
-    in if nb_marks>0 
-       then true
-       else let isc = List.fold_left (fun r y -> if r then true 
-      	       	       	       	     else if !(List.assoc y marks)=AlreadyVisited 
-      	       	       	       	       	  then false
-				          else (df_cycle_rec y)) false nx 
-	    in if isc then true
-	              else ((List.assoc x marks) := AlreadyVisited; false)
-  and df_init ls = match ls with
-        (s::lls) -> if (!(List.assoc s marks)=NotMarked)
-      	       	       & ((List.length (List.assoc s g))>0)
-      	       	    then (if df_cycle_rec s
-	                  then true
-		          else df_init lls)
-		    else df_init lls
-      | [] -> false
-  in df_init v;;
-
-let have_cycle g =
-     let v = List.map (fun (x,_) -> x) g
-  in let marks = List.map (fun x -> (x,ref NotMarked)) v
-  in if List.length g<2
-     then false
-     else let x0 = fst (List.hd g)
-          in df_cycle v marks g;;
-
-(*  Examples...
-
-  have_cycle [(1,[2;3]); (2,[3]); (3,[])];;    		(false)
-  
-  have_cycle [(1,[2;3]); (2,[1;3]); (3,[1;2])];;	(true)
-
-  have_cycle [(1 , [6]);
-      	      (2 , [3;4;5]);
-	      (3 , [2;5]);
-	      (4 , [2]);
-	      (5 , [2;3]);
-	      (6 , [1])];;			    	(true)
-
-  have_cycle [(2,[3]); (4,[]); (1,[4]); (3,[])];;       (false)
-
-  have_cycle [(3,[1;2]); (4,[]); (2,[4]); (1,[4])];;    (false)
-
-*)
-
-