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 | |
| 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')
| -rw-r--r-- | toplevel/command.ml | 4 | ||||
| -rw-r--r-- | toplevel/metasyntax.mli | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 4 |
3 files changed, 4 insertions, 6 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 = diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 216d033819..44e7133e29 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -43,7 +43,7 @@ val add_notation_interpretation : (** Add a notation interpretation for supporting the "where" clause *) -val set_notation_for_interpretation : Constrintern.full_internalization_env -> +val set_notation_for_interpretation : Constrintern.internalization_env -> (lstring * constr_expr * scope_name option) -> unit (** Add only the parsing/printing rule of a notation *) diff --git a/toplevel/record.ml b/toplevel/record.ml index 12843da60d..5107ee2ac1 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -30,7 +30,6 @@ open Topconstr (********** definition d'un record (structure) **************) let interp_evars evdref env impls k typ = - let impls = set_internalization_env_params impls [] in let typ' = intern_gen true ~impls !evdref env typ in let imps = Implicit_quantifiers.implicits_of_rawterm typ' in imps, Pretyping.Default.understand_tcc_evars evdref env k typ' @@ -46,8 +45,7 @@ let interp_fields_evars evars env nots l = | Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: impls in let d = (i,b',t') in - let impls' = set_internalization_env_params impls [] in - List.iter (Metasyntax.set_notation_for_interpretation impls') no; + List.iter (Metasyntax.set_notation_for_interpretation impls) no; (push_rel d env, impl :: uimpls, d::params, impls)) (env, [], [], []) nots l |