From 408a1d674962625dfa90d45bc17f319d3e43c7ff Mon Sep 17 00:00:00 2001
From: mohring
Date: Mon, 4 Dec 2000 07:55:31 +0000
Subject: Ajout de constr_of_string

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1044 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/base_include | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'dev/base_include')

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);;
-- 
cgit v1.2.3