Ajout de constr_of_string

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1044 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/dev/base_include b/dev/base_include
index 9405f0b98d..b73f452064 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -47,6 +47,12 @@ let e s = Astterm.interp_rawconstr Evd.empty (Global.env()) (parse_ast s);;
 (* For compatibility *)
 let raw_constr_of_string = e;;
 
+(* build a term of type constr with type-checking and resolution of 
+   implicit syntax *)
+
+let constr_of_string s 
+	= Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
+
 (* Get the current goal *)
 
 let getgoal x = top_goal_of_pftreestate (Pfedit.get_pftreestate x);;