diff options
| author | herbelin | 2010-07-22 21:06:11 +0000 |
|---|---|---|
| committer | herbelin | 2010-07-22 21:06:11 +0000 |
| commit | 1f798216ede7e3813d75732fbebc1f8fbf6622c5 (patch) | |
| tree | 3a521a550e63dca3a2e04e144de16a78f385246d /toplevel/command.ml | |
| parent | 9b4927d7fdbbafa7ed372e152e7106b3055dfb99 (diff) | |
Simplified the way internalization_data (i.e. bindings of bound vars
to their signature of implicit positions and scopes) is computed.
A bit of documentation in constrintern.mli.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13315 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index a16afa86ce..d71e586556 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -241,7 +241,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = (* Compute interpretation metadatas *) let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in let arities = List.map fst arities in - let impls = compute_full_internalization_env env0 Inductive params indnames fullarities indimpls in + let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = @@ -516,7 +516,7 @@ let interp_recursive isfix fixl notations = let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) - let impls = compute_full_internalization_env env Recursive [] fixnames fixtypes fiximps in + let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = |