diff options
| author | herbelin | 2006-10-06 08:31:08 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-06 08:31:08 +0000 |
| commit | ea1cb421a9891df15cc8e60f130fc329a11c8d3a (patch) | |
| tree | 5a5e166b452423d19ff4b9d64ad25079bcdec0b6 /interp/constrextern.ml | |
| parent | e4c48f3da68f3c3f8d0e9dada278120004eb8970 (diff) | |
Annulation de l'essai de changement de sémantique du %scope (révision 9208).
Retour à une sémantique où les %scope s'appliquent à la
sous-expression complète (trop de pbs: constantes polymorphes sans
arguments scope, variables locales de type fonctionnel, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9218 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8c81e066ad..600392811b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -360,9 +360,6 @@ let make_pat_notation loc ntn l = (fun (loc,p) -> CPatPrim (loc,p)) destPatPrim l -let find_arguments_scope ref = - List.map (option_map (fun sc -> LightTmpScope sc)) (find_arguments_scope ref) - let bind_env sigma var v = try let vvar = List.assoc var sigma in @@ -445,9 +442,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> - let scopes' = - if (* recursive *) false then option_cons scopt scopes - else scopes in + let scopes' = option_cons scopt scopes in let l = List.map (fun (c,(scopt,scl)) -> extern_cases_pattern_in_scope (scopt,scl@scopes') vars c) @@ -755,7 +750,7 @@ let rec extern inctx scopes vars r = | RDynamic (loc,d) -> CDynamic (loc,d) and extern_typ (_,scopes) = - extern true (Some (LightTmpScope (Notation.type_scope)),scopes) + extern true (Some Notation.type_scope,scopes) and sub_extern inctx (_,scopes) = extern inctx (None,scopes) @@ -823,9 +818,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> - let scopes' = - if (* recursive *) false then option_cons scopt scopes - else scopes in + let scopes' = option_cons scopt scopes in let l = List.map (fun (c,(scopt,scl)) -> extern (* assuming no overloading: *) true @@ -866,7 +859,7 @@ let extern_constr_gen at_top scopt env t = extern (not at_top) (scopt,[]) vars r let extern_constr_in_scope at_top scope env t = - extern_constr_gen at_top (Some (ExplicitTmpScope scope)) env t + extern_constr_gen at_top (Some scope) env t let extern_constr at_top env t = extern_constr_gen at_top None env t |