diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 18 | ||||
| -rw-r--r-- | interp/constrintern.mli | 2 |
2 files changed, 20 insertions, 0 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 357ce43774..c658faa0f4 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1236,6 +1236,24 @@ let interp_casted_constr sigma env ?(impls=([],[])) c typ = let interp_open_constr sigma env c = Default.understand_tcc sigma env (intern_constr sigma env c) +let interp_open_constr_patvar sigma env c = + let raw = intern_gen false sigma env c ~allow_patvar:true in + let sigma = ref (Evd.create_evar_defs sigma) in + let evars = ref (Gmap.empty : (identifier,rawconstr) Gmap.t) in + let rec patvar_to_evar r = match r with + | RPatVar (loc,(_,id)) -> + ( try Gmap.find id !evars + with Not_found -> + let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in + let ev = Evarutil.e_new_evar sigma env ev in + let rev = REvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in + evars := Gmap.add id rev !evars; + rev + ) + | _ -> map_rawconstr patvar_to_evar r in + let raw = patvar_to_evar raw in + Default.understand_tcc (Evd.evars_of !sigma) env raw + let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 6410c9b2ee..126eff8596 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -87,6 +87,8 @@ val interp_type : evar_map -> env -> ?impls:full_implicits_env -> val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr +val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * constr + val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> constr_expr -> types -> constr |