diff options
| author | delahaye | 2001-06-18 12:49:42 +0000 |
|---|---|---|
| committer | delahaye | 2001-06-18 12:49:42 +0000 |
| commit | 6d8328ec5e7dad8d5347cce5d7ce5a699381671c (patch) | |
| tree | 10637cd7bbf2162540acebd42b4add857f6acbe5 /proofs | |
| parent | 7fd05ed06e94e5411755d76a5b612962f3fdab6b (diff) | |
Interpretation MetaId + Progress + Inst
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1789 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacinterp.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 6730419a99..6b0078b4c1 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -443,7 +443,7 @@ let rec make_subs_list = function | [] -> [] (* Debug reference *) -let debug =ref DebugOff +let debug = ref DebugOff (* Sets the debugger mode *) let set_debug pos = debug := pos @@ -479,6 +479,8 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast = | Node(_,"IDTAC",[]) -> VTactic tclIDTAC | Node(_,"FAIL",[]) -> VTactic (tclFAIL 0) | Node(_,"FAIL",[n]) -> VTactic (tclFAIL (num_of_ast n)) + | Node(_,"PROGRESS",[tac]) -> + VTactic (tclPROGRESS (tac_interp lfun lmatch debug tac)) | Node(_,"TACTICLIST",l) -> VTactic (interp_semi_list tclIDTAC lfun lmatch debug l) | Node(_,"DO",[n;tac]) -> @@ -512,6 +514,11 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast = with | Not_found -> (try (vcontext_interp (evc,env,lfun,lmatch,goalopt,debug) (lookup s)) with | Not_found -> VArg (Identifier (id_of_string s)))) + | Node(loc,"METAID",[Num(_,n)]) -> + (try VArg (Identifier (destVar (List.assoc n lmatch))) with + | Invalid_argument "destVar" -> + user_err_loc (loc, "Tacinterp.val_interp",[<'sTR + "Metavariable "; 'iNT n; 'sTR " must be an identifier" >])) | Str(_,s) -> VArg (Quoted_string s) | Num(_,n) -> VArg (Integer n) | Node(_,"COMMAND",[c]) -> |