diff options
| -rw-r--r-- | interp/constrintern.ml | 41 | ||||
| -rw-r--r-- | interp/constrintern.mli | 9 |
2 files changed, 49 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index aa9a379db..76d0a1bf6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1100,6 +1100,21 @@ let interp_open_constr sigma env c = let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) + +let interp_constr_evars_gen isevars env ?(impls=([],[])) kind c = + Default.understand_tcc_evars isevars env kind + (intern_gen (kind=IsType) ~impls (Evd.evars_of !isevars) env c) + +let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ = + interp_constr_evars_gen isevars env ~impls (OfType (Some typ)) c + +let interp_type_evars isevars env ?(impls=([],[])) c = + interp_constr_evars_gen isevars env IsType ~impls c + +let interp_constr_judgment_evars isevars env c = + Default.understand_judgment_tcc isevars env + (intern_constr (Evd.evars_of !isevars) env c) + type ltac_sign = identifier list * unbound_ltac_var_map let interp_constrpattern sigma env c = @@ -1123,7 +1138,13 @@ let interp_aconstr impls vars a = let interp_binder sigma env na t = let t = intern_gen true sigma env t in - Default.understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t) + let t' = locate_if_isevar (loc_of_rawconstr t) na t in + Default.understand_type sigma env t' + +let interp_binder_evars isevars env na t = + let t = intern_gen true (Evd.evars_of !isevars) env t in + let t' = locate_if_isevar (loc_of_rawconstr t) na t in + Default.understand_tcc_evars isevars env IsType t' open Environ open Term @@ -1146,6 +1167,24 @@ let interp_context sigma env params = (push_rel d env,d::params)) (env,[]) params +let interp_context_evars isevars env params = + List.fold_left + (fun (env,params) d -> match d with + | LocalRawAssum ([_,na],(CHole _ as t)) -> + let t = interp_binder_evars isevars env na t in + let d = (na,None,t) in + (push_rel d env, d::params) + | LocalRawAssum (nal,t) -> + let t = interp_type_evars isevars env t in + let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in + let ctx = List.rev ctx in + (push_rel_context ctx env, ctx@params) + | LocalRawDef ((_,na),c) -> + let c = interp_constr_judgment_evars isevars env c in + let d = (na, Some c.uj_val, c.uj_type) in + (push_rel d env,d::params)) + (env,[]) params + (**********************************************************************) (* Locating reference, possibly via an abbreviation *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 70af93885..4603565e3 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -76,6 +76,12 @@ val interp_type : evar_map -> env -> ?impls:full_implicits_env -> val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr +val interp_casted_constr_evars : evar_defs ref -> env -> + ?impls:full_implicits_env -> constr_expr -> types -> constr + +val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> + constr_expr -> types + (*s Build a judgment *) val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment @@ -95,6 +101,9 @@ val interp_binder : evar_map -> env -> name -> constr_expr -> types val interp_context : evar_map -> env -> local_binder list -> env * rel_context +val interp_context_evars : + evar_defs ref -> env -> local_binder list -> env * rel_context + (* Locating references of constructions, possibly via a syntactic definition *) val locate_reference : qualid -> global_reference |