From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 tactics/elim.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'tactics/elim.ml')

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 889ead5e..55df0f0a 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: elim.ml 9842 2007-05-20 17:44:23Z herbelin $ *)
+(* $Id: elim.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -49,8 +49,8 @@ let introCaseAssumsThen tac ba =
     else 
       (ba.branchnames, []),
        if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in
-  let introCaseAssums = tclTHEN (intros_pattern None l1) (intros_clearing l3)
-  in
+  let introCaseAssums =
+    tclTHEN (intros_pattern no_move l1) (intros_clearing l3) in
   (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
 
 (* The following tactic Decompose repeatedly applies the
@@ -115,7 +115,7 @@ let inductive_of = function
   | IndRef ity -> ity
   | r ->
       errorlabstrm "Decompose"
-        (Printer.pr_global r ++ str " is not an inductive type")
+        (Printer.pr_global r ++ str " is not an inductive type.")
 
 let decompose_these c l gls =
   let indl = (*List.map inductive_of*) l in 
@@ -182,7 +182,7 @@ let double_ind h1 h2 gls =
   let (abs_i,abs_j) =
     if abs_i < abs_j then (abs_i,abs_j) else
     if abs_i > abs_j then (abs_j,abs_i) else
-      error "Both hypotheses are the same" in
+      error "Both hypotheses are the same." in
   (tclTHEN (tclDO abs_i intro)
      (onLastHyp
        	(fun id ->
-- 
cgit v1.2.3