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 | |
| 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
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/constrintern.mli | 1 | ||||
| -rw-r--r-- | toplevel/command.ml | 2 |
3 files changed, 6 insertions, 1 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 diff --git a/toplevel/command.ml b/toplevel/command.ml index 1c636275a4..8279c14527 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -186,7 +186,7 @@ let interp_mutual lparams lnamearconstrs finite = let env_params, params = List.fold_left (fun (env, params) (id,t) -> - let p = interp_type sigma env t in + let p = interp_binder sigma env (Name id) t in (Termops.push_rel_assum (Name id,p) env, (Name id,None,p)::params)) (env0,[]) lparams in |