diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-20 08:39:46 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-20 08:39:46 +0000 |
| commit | 31c8f44cfd250b0b4d77a25bf4339f4fab2f55c0 (patch) | |
| tree | 6ea135784db070ba14b6f41e64503892fe13e1e4 /proofs | |
| parent | c4f2c5bd37f17352c0f02c3ef54de541c5c09b89 (diff) | |
Prise en compte noms longs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@857 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacinterp.ml | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index f45d896d4..6940f2a07 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -136,11 +136,16 @@ let overwriting_interp_add (ast_typ,interp_fun) = let look_for_interp = Hashtbl.find interp_tab (* Globalizes the identifier *) -let glob_nvar id = +let glob_const_nvar loc id = + let sp = make_path [] id CCI in try - Nametab.sp_of_id CCI id + match Nametab.locate sp with + | ConstRef sp -> sp + | _ -> error ((string_of_path sp) ^ " does not denote a constant") with - | Not_found -> error ("unbound variable " ^ (string_of_id id)) + | Not_found -> + Pretype_errors.error_global_not_found_loc loc sp + (* Summary and Object declaration *) let mactab = ref Gmap.empty @@ -823,8 +828,9 @@ and cvt_pattern (evc,env,lfun,lmatch,goalopt,debug) = function | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern") and cvt_unfold (evc,env,lfun,lmatch,goalopt,debug) = function - | Node(_,"UNFOLD", com::nums) -> - (List.map num_of_ast nums,glob_nvar (id_of_Identifier (unvarg (val_interp + | Node(loc,"UNFOLD", com::nums) -> + (List.map num_of_ast nums, + glob_const_nvar loc (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug) com)))) | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold") @@ -844,12 +850,14 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf = (match lf with | Node(loc,"Unf",l)::lf -> let idl= - List.map (fun v -> glob_nvar (id_of_Identifier (unvarg + List.map + (fun v -> glob_const_nvar loc (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l in add_flag (red_add red (CONST idl)) lf | Node(loc,"UnfBut",l)::lf -> let idl= - List.map (fun v -> glob_nvar (id_of_Identifier (unvarg + List.map + (fun v -> glob_const_nvar loc (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l in add_flag (red_add red (CONSTBUT idl)) lf | _ -> add_flag (red_add red DELTA) lf) |