diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-17 09:00:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-17 09:00:42 +0000 |
| commit | b8cd60cf1b3817a1802459310e79a8addb628ee7 (patch) | |
| tree | 8af3fe252c2de280791c57d3fd68f1aaa6a10ef9 /dev | |
| parent | e6c8c552cff89a45e696261aec441bf690a3e963 (diff) | |
Prise en compte du renommage des fonctions de Astterm
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@361 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/dev/base_include b/dev/base_include index 90ad20402..9405f0b98 100644 --- a/dev/base_include +++ b/dev/base_include @@ -39,15 +39,13 @@ let parse_tac = Pcoq.parse_string Pcoq.Tactic.tactic;; (* For compatibility reasons *) let parse_ast = parse_com;; -(* build a term of type constr without type-checking or resolution of +(* build a term of type rawconstr without type-checking or resolution of implicit syntax *) -let raw_constr_of_string s = - Astterm.dbize_cci Evd.empty (unitize_env (Global.context())) - (parse_ast s);; +let e s = Astterm.interp_rawconstr Evd.empty (Global.env()) (parse_ast s);; -let e s = - Astterm.constr_of_com Evd.empty (Global.env()) (parse_ast s);; +(* For compatibility *) +let raw_constr_of_string = e;; (* Get the current goal *) @@ -57,7 +55,7 @@ let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());; let current_goal () = get_nth_goal 1;; let pf_e gl s = - Astterm.constr_of_com (project gl) (pf_env gl) (parse_ast s);; + Astterm.interp_constr (project gl) (pf_env gl) (parse_ast s);; open Toplevel let go = loop |