diff options
| author | Hugo Herbelin | 2017-05-21 22:23:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 00:44:26 +0200 |
| commit | ca630605330828b9b6456477b0fd4f8a0c3f1831 (patch) | |
| tree | e04712936c193bbe5daade5843f9f8eb5a8c38fc /vernac | |
| parent | 09e15424aab082fd4b18a06e8894227beddeb487 (diff) | |
More precise on preventing clash between bound vars name and hidden impargs.
We want to avoid capture in "Inductive I {A} := C : forall A, I".
But in "Record I {A} := { C : forall A, A }.", non recursivity ensures
that no clash will occur.
This fixes previous commit, with which it could possibly be merged.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 7 |
2 files changed, 5 insertions, 4 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 02d8525158..0064af77d2 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -603,7 +603,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let indimpls = List.map (fun (_, _, impls) -> userimpls @ lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in - let impls = compute_internalization_env env0 ~impls (Inductive params) indnames fullarities indimpls in + let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in diff --git a/vernac/record.ml b/vernac/record.ml index a220e515e7..88f4586800 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -94,7 +94,7 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl -let typecheck_params_and_fields def id pl t ps nots fs = +let typecheck_params_and_fields finite def id pl t ps nots fs = let env0 = Global.env () in let ctx = Evd.make_evar_universe_context env0 pl in let evars = ref (Evd.from_ctx ctx) in @@ -139,7 +139,8 @@ let typecheck_params_and_fields def id pl t ps nots fs = let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in let assums = List.filter is_local_assum newps in let params = List.map (RelDecl.get_name %> out_name) assums in - let impls_env = compute_internalization_env env0 ~impls:impls_env (Inductive params) [id] [EConstr.to_constr !evars arity] [imps] in + let ty = Inductive (params,(finite != BiFinite)) in + let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr !evars arity] [imps] in let env2,impls,newfs,data = interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs) in @@ -563,7 +564,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id (* Now, younger decl in params and fields is on top *) let (pl, ctx), arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> - typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in + typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in let sign = structure_signature (fields@params) in let gr = match kind with | Class def -> |