diff options
| author | herbelin | 2003-03-29 14:33:17 +0000 |
|---|---|---|
| committer | herbelin | 2003-03-29 14:33:17 +0000 |
| commit | cde6f21cd5cf45303f597bcda5b4a377ef93e74a (patch) | |
| tree | a0a2a89a440581dc91b3aae4edec6e754b9dd1d1 /interp | |
| parent | 22b3af749027a819964a3639498a4ce53b34be01 (diff) | |
Implicit Variables Type dans les inductive
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3808 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/constrintern.mli | 1 |
2 files changed, 5 insertions, 0 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 9ab3ddf42f..b476320150 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -590,6 +590,10 @@ let interp_casted_openconstr sigma env c typ = let interp_type sigma env c = understand_type sigma env (interp_rawtype sigma env c) +let interp_binder sigma env na t = + let t = interp_rawtype sigma env t in + understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t) + let interp_type_with_implicits sigma env impls c = understand_type sigma env (interp_rawtype_with_implicits sigma env impls c) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 5478957b56..5d66424c24 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -49,6 +49,7 @@ val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env -> val interp_constr : evar_map -> env -> constr_expr -> constr val interp_casted_constr : evar_map -> env -> constr_expr -> types -> constr val interp_type : evar_map -> env -> constr_expr -> types +val interp_binder : evar_map -> env -> name -> constr_expr -> types val interp_openconstr : evar_map -> env -> constr_expr -> evar_map * constr val interp_casted_openconstr : evar_map -> env -> constr_expr -> constr -> evar_map * constr |