diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
| commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
| tree | 0c647056de1832cf1dba5ba58758b9121418e4be /tactics/elim.ml | |
| parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) | |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 10 |
1 files changed, 5 insertions, 5 deletions
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 -> |