aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-23 21:09:30 +0000
committerGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-11-23 21:09:30 +0000
commit897faf0719a7f457eb12c08c948683064c09103d (patch)
treee2deaadf9230b9dbe3ddd47be63e0c60e9b7a587 /proofs
parent4eae8b2e19d8ea1fc527216b9bfbab93803af313 (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.ml41
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