From 469975942e7ce58127286e05adba06afe2fdd8e9 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Fri, 21 Sep 2001 15:46:47 +0000
Subject: Correction due au changement de semantique de Match

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2049 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacinterp.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 098c2568e0..cb1fb94148 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -463,7 +463,6 @@ let set_debug pos = debug := pos
 (* Gives the state of debug *)
 let get_debug () = !debug
 
-
 (* Interprets any expression *)
 let rec val_interp ist ast =
 
@@ -899,10 +898,9 @@ and match_interp ist ast lmr =
     | _ ->
       errorlabstrm "Tacinterp.apply_match" [<'sTR
         "No matching clauses for Match">] in
-  let csr =
-    constr_of_Constr (unvarg (val_interp ist (List.hd lmr)))
-  and ilr = read_match_rule
-    ist.evc ist.env (constr_list ist.goalopt ist.lfun) (List.tl lmr) in
+  let csr = constr_of_Constr (unvarg (val_interp ist (List.hd lmr)))
+  and ilr = read_match_rule ist.evc ist.env (constr_list ist.goalopt ist.lfun)
+    (List.tl lmr) in
   apply_match ist csr ilr
 
 and tactic_interp ist ast g =
-- 
cgit v1.2.3