diff options
author | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-23 21:09:30 +0000 |
---|---|---|
committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-23 21:09:30 +0000 |
commit | 897faf0719a7f457eb12c08c948683064c09103d (patch) | |
tree | e2deaadf9230b9dbe3ddd47be63e0c60e9b7a587 /proofs | |
parent | 4eae8b2e19d8ea1fc527216b9bfbab93803af313 (diff) |
Correction d'un bug lorsque des Variables sont clearees dans le but courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@935 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/tacinterp.ml | 41 |
1 files changed, 29 insertions, 12 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 29daa7965..422d41222 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -63,17 +63,28 @@ let make_hyps = List.map (fun (id,_,typ) -> (string_of_id id,body_of_type typ)) let rec constr_list goalopt = function | (str,VArg(Constr c))::tl -> (id_of_string str,c)::(constr_list goalopt tl) | (str,VArg(Identifier id))::tl -> - (try - (id_of_string str,Declare.global_reference CCI id)::(constr_list - goalopt tl) - with | Not_found -> - (match goalopt with - | None -> constr_list goalopt tl - | Some goal -> - if mem_named_context id (pf_hyps goal) then - (id_of_string str,mkVar id)::(constr_list goalopt tl) - else - constr_list goalopt tl)) + (match goalopt with + | None -> constr_list goalopt tl + | Some goal -> + let hyps = pf_hyps goal in + (try + let csr = Declare.global_reference CCI id in + (match kind_of_term csr with + | IsVar idc -> + if mem_named_context idc hyps then + (id_of_string str,Declare.global_reference CCI id):: + (constr_list goalopt tl) + else + constr_list goalopt tl + | _ -> + (id_of_string str,Declare.global_reference CCI id):: + (constr_list goalopt tl)) + with + | Not_found -> + if mem_named_context id (pf_hyps goal) then + (id_of_string str,mkVar id)::(constr_list goalopt tl) + else + constr_list goalopt tl)) | _::tl -> constr_list goalopt tl | [] -> [] @@ -437,6 +448,13 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast = with | Not_found -> (try (lookup s) with | Not_found -> VArg (Identifier (id_of_string s)))) + + | Node(_,"QUALID",[Nvar(_,s)]) -> + (try (unrec (List.assoc s lfun)) + with | Not_found -> + (try (lookup s) + with | Not_found -> VArg (Identifier (id_of_string s)))) + | Str(_,s) -> VArg (Quoted_string s) | Num(_,n) -> VArg (Integer n) | Node(_,"COMMAND",[c]) -> @@ -475,7 +493,6 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast = Not_found -> val_interp (evc,env,lfun,lmatch,goalopt,debug) (Node(dummy_loc,"APPTACTIC",[ast]))) - | Dynamic(_,t) -> env_update (evc,env,lfun,lmatch,goalopt,debug); let f = (ocamlOut t) in |