diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-18 17:51:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-18 17:51:58 +0000 |
| commit | edfda2501f08f18e24bd2e3eca763eb1c2dec0ea (patch) | |
| tree | e4c42c670c2f61b95a7a0f68fd96f635aeef8b2b /toplevel/record.ml | |
| parent | a586cb418549eb523a3395155cab2560fd178571 (diff) | |
Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 321f9bf31..38d9e670d 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -66,22 +66,22 @@ let all_vars t = let print_id_list l = [< 'sTR "[" ; prlist_with_sep pr_coma print_id l; 'sTR "]" >] +open Environ + let typecheck_params_and_field ps fs = let env0 = Global.env () in let env1,newps = List.fold_left (fun (env,newps) (id,t) -> - let tj = type_judgment_of_rawconstr Evd.empty env t in - let ass = Typeops.assumption_of_type_judgment tj in - (Environ.push_named_assum (id,ass) env,(id,tj.Environ.utj_val)::newps)) + let tj = interp_type Evd.empty env t in + (push_named_assum (id,tj) env,(id,tj)::newps)) (env0,[]) ps in let env2,newfs = List.fold_left (fun (env,newfs) (id,t) -> - let tj = type_judgment_of_rawconstr Evd.empty env t in - let ass = Typeops.assumption_of_type_judgment tj in - (Environ.push_named_assum (id,ass) env,(id,tj.Environ.utj_val)::newfs)) (env1,[]) fs + let ass = interp_type Evd.empty env t in + (push_named_assum (id,ass) env,(id,ass)::newfs)) (env1,[]) fs in List.rev(newps),List.rev(newfs) |