diff options
author | 2006-09-01 11:38:36 +0000 | |
---|---|---|
committer | 2006-09-01 11:38:36 +0000 | |
commit | 6b3ca56999aa2fd3ff6a86773f6a4273c45dbf81 (patch) | |
tree | 3da347b6418b4ff5ec5bdf722ab3dc5f5db94bbb /interp/constrintern.ml | |
parent | 1fe97f12f24f596ab2408348e7556d483ed58e96 (diff) |
Export de fonctions d'interprétation acceptant des evars non résolues
en entrée et en sortie
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9107 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r-- | interp/constrintern.ml | 41 |
1 files changed, 40 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 *) |