From 763cf4f37e10d9a0e8a2a0e9286c02708a60bf08 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 16 Jul 2004 20:01:26 +0000
Subject: Nouvelle en-tête

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/blast.ml     | 2 +-
 contrib/interface/showproof.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index a7e98b69dc..d5236a7a9f 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -506,7 +506,7 @@ let full_auto n gl =
   tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
   
 let default_full_auto gl = full_auto !default_search_depth gl
-(***********************************************************************)
+(************************************************************************)
 
 let blast_tactic = ref (free_try default_full_auto)
 ;;
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 5918a8b7ee..5b265ec864 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1676,7 +1676,7 @@ and natural_induction ig lh g gs ge arg2 ltree with_intros=
                     ])
                   ltree))
         ]
-(***********************************************************************)
+(************************************************************************)
 (* Points fixes *)
 
 and natural_fix ig lh g gs narg ltree =
-- 
cgit v1.2.3