diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/astterm.ml | 12 | ||||
| -rw-r--r-- | parsing/astterm.mli | 4 |
2 files changed, 15 insertions, 1 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index e8eb9c3e4a..b595c901f8 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 04da5c0e6d..8f844e6006 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 |