diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-16 15:58:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-16 15:58:48 +0000 |
| commit | 3c248785237d8dea037da274f4acc0229894de93 (patch) | |
| tree | 4501aca5e725d5f62ffd9f959a8956f30bf432eb /tactics/auto.ml | |
| parent | 649e7e98e0067a7ae2a3990b9629dcec66b47497 (diff) | |
ident au lieu de string pour le nom de base de qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 7a9ba72b9..e2e719a1d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -421,7 +421,7 @@ let _ = let hyps = Declare.implicit_section_args ref in let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in let _,i = repr_qualid qid in - (id_of_string i, applist (c,section_args)) + (i, applist (c,section_args)) | _-> bad_vernac_args "HintsResolve") lh in let dbnames = if l = [] then ["core"] else List.map (function VARG_IDENTIFIER i -> string_of_id i @@ -438,7 +438,7 @@ let _ = List.map (function | VARG_QUALID qid -> let _,n = repr_qualid qid in - (id_of_string n, global qid) + (n, global qid) | _ -> bad_vernac_args "HintsUnfold") lh in let dbnames = if l = [] then ["core"] else List.map (function @@ -462,7 +462,7 @@ let _ = let c = Declare.constr_of_reference Evd.empty env ref in let hyps = Declare.implicit_section_args ref in let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in - (id_of_string n, applist (c, section_args)) + (n, applist (c, section_args)) | _ -> bad_vernac_args "HintsImmediate") lh in let dbnames = if l = [] then ["core"] else List.map (function @@ -956,7 +956,7 @@ let cvt_autoArgs = let interp_to_add gl = function | (Qualid qid) -> let _,id = repr_qualid qid in - (next_ident_away (id_of_string id) (pf_ids_of_hyps gl), + (next_ident_away id (pf_ids_of_hyps gl), Declare.constr_of_reference Evd.empty (Global.env()) (global qid)) | _ -> errorlabstrm "cvt_autoArgs" [< 'sTR "Qualid expected" >] |