- global_reference traite des variables

 - construct_reference, avec environnement en argument
 - link de Class
 - Definition et Check au toplevel


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

2 files changed, 15 insertions, 1 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index e8eb9c3e4..b595c901f 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -148,7 +148,7 @@ let dbize_ref k sigma env loc s =
 	| FW  -> Declare.global_reference_imps FW id
 	| OBJ -> anomaly "search_ref_cci_fw" in
       RRef (loc,ref_from_constr c), il
-    with UserError _ ->
+    with Not_found ->
       try 
 	(Syntax_def.search_syntactic_definition id, [])
       with Not_found -> 
@@ -465,6 +465,16 @@ let fconstr_of_com_env1 is_ass sigma env com =
 let fconstr_of_com_env sigma hyps com =
   fconstr_of_com_env1 false sigma hyps com 
     
+let judgment_of_com1 is_ass sigma env com = 
+  let c = raw_constr_of_com sigma (context env) com in
+  try 
+    ise_resolve is_ass sigma [] env c
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
+
+let judgment_of_com sigma env com =
+  judgment_of_com1 false sigma env com
+
 (* Without dB *)
 let type_of_com env com =
   let sign = context env in
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 04da5c0e6..8f844e600 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -51,6 +51,10 @@ val fconstr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr
 val fconstr_of_com : 'a evar_map -> env -> Coqast.t -> constr
 val fconstr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
 
+val judgment_of_com1 : 
+  bool -> 'a evar_map -> env -> Coqast.t -> unsafe_judgment
+val judgment_of_com : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
+
 (* Typing with Trad, and re-checking with Mach *)
 (*i
 val fconstruct :'c evar_map -> context -> Coqast.t -> unsafe_judgment