diff options
| author | filliatr | 2000-07-20 16:46:15 +0000 |
|---|---|---|
| committer | filliatr | 2000-07-20 16:46:15 +0000 |
| commit | b6337996e891f3fa33e0ff01a7dae13c469d6055 (patch) | |
| tree | 119d52ec97de7ad8e56d9b5c74373e3a4fd5a954 /proofs | |
| parent | f8a0d5e7f5efcd588627a2eadeb6e8f9f7d597c6 (diff) | |
portage Refine
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@559 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacinterp.ml | 40 |
1 files changed, 24 insertions, 16 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 4340aa31db..c01a547d6a 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -546,30 +546,38 @@ and bind_interp evc env lfun lmatch goalopt = function errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding"; print_ast x>] -(* Interprets a COMMAND expression *) +(* Interprets a COMMAND expression (in case of failure, returns Command) *) and com_interp (evc,env,lfun,lmatch,goalopt) = function | Node(_,"EVAL",[c;rtc]) -> let redexp = unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) rtc)) in VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr1 evc env (make_subs_list lfun) lmatch c))) - | c -> VArg (Constr (interp_constr1 evc env (make_subs_list lfun) lmatch c)) + | c -> + try + VArg (Constr (interp_constr1 evc env (make_subs_list lfun) lmatch c)) + with e when Logic.catchable_exception e -> + VArg (Command c) (* Interprets a CASTEDCOMMAND expression *) -and cast_com_interp (evc,env,lfun,lmatch,goalopt) com = - match goalopt with - Some gl -> - (match com with - | Node(_,"EVAL",[c;rtc]) -> - let redexp = unredexp (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt) rtc)) in - VArg (Constr ((reduction_of_redexp redexp) env evc - (interp_casted_constr1 evc env (make_subs_list lfun) lmatch c - (pf_concl gl)))) - | c -> - VArg (Constr (interp_casted_constr1 evc env (make_subs_list lfun) - lmatch c (pf_concl gl)))) - | None -> +and cast_com_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with + | Some gl -> + (match com with + | Node(_,"EVAL",[c;rtc]) -> + let redexp = + unredexp (unvarg (val_interp + (evc,env,lfun,lmatch,goalopt) rtc)) + in + VArg (Constr ((reduction_of_redexp redexp) env evc + (interp_casted_constr1 evc env + (make_subs_list lfun) lmatch c (pf_concl gl)))) + | c -> + try + VArg (Constr (interp_casted_constr1 evc env + (make_subs_list lfun) lmatch c (pf_concl gl))) + with e when Logic.catchable_exception e -> + VArg (Command c)) + | None -> errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">] and cvt_pattern (evc,env,lfun,lmatch,goalopt) = function |