diff options
| author | delahaye | 2001-09-21 15:46:47 +0000 |
|---|---|---|
| committer | delahaye | 2001-09-21 15:46:47 +0000 |
| commit | 469975942e7ce58127286e05adba06afe2fdd8e9 (patch) | |
| tree | 4ce6b2fa84cd0720cf225f848011214d78df6a0a /proofs | |
| parent | 41278f9af1a4db0682d619b7469ef8274f4437d4 (diff) | |
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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacinterp.ml | 8 |
1 files changed, 3 insertions, 5 deletions
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 = |