From 8d595e0592972d29ccf4cbbd6b61f6b1aa06a952 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Wed, 28 Jun 2000 14:33:06 +0000
Subject: Modifs de presentation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@520 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/auto.ml  | 2 +-
 tactics/eauto.ml | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 2a98b8e2fb..067d610fec 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -510,7 +510,7 @@ let fmt_hint_term cl =
     in 
     if valid_dbs = [] then 
       [<'sTR "No hint applicable for current goal" >]
-    else 
+    else
       [< 'sTR "Applicable Hints :";
 	 prlist (fun (name,db,hintlist) ->
 	 	   [< 'sTR "  In the database "; 'sTR name; 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 69d4e59c62..74d49114ba 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -16,8 +16,7 @@ open Pattern
 open Clenv
 open Auto
 
-let e_give_exact c gl =
-  tclTHEN (unify (pf_type_of gl c)) (Tactics.exact c) gl
+let e_give_exact c gl = tclTHEN (unify (pf_type_of gl c)) (Tactics.exact c) gl
 
 let assumption id = e_give_exact (VAR id)
         
-- 
cgit v1.2.3