aboutsummaryrefslogtreecommitdiff
path: root/toplevel/record.ml
diff options
context:
space:
mode:
authorherbelin2000-03-28 16:27:35 +0000
committerherbelin2000-03-28 16:27:35 +0000
commitbc8d450ec17b6e9f40aae2ad040f296ed2f3419f (patch)
tree3a1f82207e8b30a68d74aef88e41853f4aa55d3e /toplevel/record.ml
parent45e7f49dcbea582e06786a95cd636cd7f163d3c6 (diff)
Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en interp_constr etc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@356 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/record.ml')
-rw-r--r--toplevel/record.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 79ccb76111..673f4a4f61 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -70,14 +70,14 @@ let typecheck_params_and_field ps fs =
let env1,newps =
List.fold_left
(fun (env,newps) (id,t) ->
- let tj = type_of_com env t in
+ let tj = typed_type_of_com Evd.empty env t in
(Environ.push_var (id,tj) env,(id,tj.body)::newps))
(env0,[]) ps
in
let env2,newfs =
List.fold_left
(fun (env,newfs) (id,t) ->
- let tj = type_of_com env t in
+ let tj = typed_type_of_com Evd.empty env t in
(Environ.push_var (id,tj) env,(id,tj.body)::newfs)) (env1,[]) fs
in
List.rev(newps),List.rev(newfs)