diff options
| author | herbelin | 2000-03-28 16:30:04 +0000 |
|---|---|---|
| committer | herbelin | 2000-03-28 16:30:04 +0000 |
| commit | ed11f59ab67b0b6eb103d07386bf45ab2a8bede6 (patch) | |
| tree | 78d2631a84485271c91909915dfa8f96f67d5ca0 /tactics/auto.ml | |
| parent | bc8d450ec17b6e9f40aae2ad040f296ed2f3419f (diff) | |
Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf_,}interp_constr*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@357 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 15e9069dda..97222bd359 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -331,7 +331,7 @@ let _ = "HintResolve" (function | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_CONSTR c] -> - let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in + let c1 = Astterm.interp_constr Evd.empty (Global.env()) c in let dbnames = if l = [] then ["core"] else List.map (function VARG_IDENTIFIER i -> string_of_id i | _ -> bad_vernac_args "HintResolve") l in @@ -343,7 +343,7 @@ let _ = "HintImmediate" (function | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_CONSTR c] -> - let c1 = Astterm.constr_of_com Evd.empty (Global.env()) c in + let c1 = Astterm.interp_constr Evd.empty (Global.env()) c in let dbnames = if l = [] then ["core"] else List.map (function VARG_IDENTIFIER i -> string_of_id i | _ -> bad_vernac_args "HintImmediate") l in |