diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-15 19:48:24 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-15 19:48:24 +0000 |
| commit | 3675bac6c38e0a26516e434be08bc100865b339b (patch) | |
| tree | 87f8eb1905c7b508dea60b1e216f79120e9e772d /tactics | |
| parent | c881bc37b91a201f7555ee021ccb74adb360d131 (diff) | |
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3434299ab..01b210ac3 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1462,8 +1462,8 @@ and match_context_interp ist g lr lmr = apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) | _ -> errorlabstrm "Tacinterp.apply_match_context" (str - "No matching clauses for Match Context") - (v 0 (str "No matching clauses for Match Context" ++ + "No matching clauses for match goal") + (v 0 (str "No matching clauses for match goal" ++ (if ist.debug=DebugOff then fnl() ++ str "(use \"Debug On\" for more info)" else mt()))) @@ -1570,9 +1570,13 @@ and match_interp ist g constr lmr = apply_match ist csr tl) | _ -> errorlabstrm "Tacinterp.apply_match" (str - "No matching clauses for Match") in + "No matching clauses for match") in let env = pf_env g in - let csr = constr_of_value env (val_interp ist g constr) in + let csr = + try constr_of_value env (val_interp ist g constr) + with Not_found -> + errorlabstrm "Tacinterp.apply_match" + (str "Argument of match does not evaluate to a term") in let ilr = read_match_rule (project g) env (fst (constr_list ist env)) lmr in apply_match ist csr ilr |