From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:01 +0200 Subject: Imported Upstream version 8.4dfsg --- interp/constrintern.ml | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1dd735ad..45df005c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* None & - (* scopes have no effect on the interpretation of identifiers, hence - we can tolerate having a variable occurring several times in - different scopes: *) typ <> NtnInternTypeIdent & - make_current_scope (Option.get !idscopes) - <> make_current_scope (env.tmp_scope,env.scopes) then - error_inconsistent_scope loc id - (make_current_scope (Option.get !idscopes)) - (make_current_scope (env.tmp_scope,env.scopes)) - else - idscopes := Some (env.tmp_scope,env.scopes); + if istermvar then + (* scopes have no effect on the interpretation of identifiers *) + if !idscopes = None then + idscopes := Some (env.tmp_scope,env.scopes) + else + if make_current_scope (Option.get !idscopes) + <> make_current_scope (env.tmp_scope,env.scopes) + then + error_inconsistent_scope loc id + (make_current_scope (Option.get !idscopes)) + (make_current_scope (env.tmp_scope,env.scopes)); match typ with | NtnInternTypeBinder -> if istermvar then error_expect_binder_notation_type loc id @@ -1682,7 +1683,7 @@ let interp_rawcontext_gen understand_type understand_judgment env bl = (push_rel d env, d::params, succ n, impls) | Some b -> let c = understand_judgment env b in - let d = (na, Some c.uj_val, c.uj_type) in + let d = (na, Some c.uj_val, Termops.refresh_universes c.uj_type) in (push_rel d env, d::params, succ n, impls)) (env,[],1,[]) (List.rev bl) in (env, par), impls -- cgit v1.2.3