diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-30 15:14:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-30 15:14:05 +0000 |
| commit | 05eb251edcca594e22cd6be3793b690dcc8bfa49 (patch) | |
| tree | 1778ed6f955bf9378a29a7294d94eab9c3bb2b1d /interp | |
| parent | a59062b279c3d173570731cafc2b5ec18c80e93a (diff) | |
Les notations hors scope s'empilent maintenant comme des scopes ne
contenant qu'une notation + renommage dans Reals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4505 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 22ff0ee31..7a557f858 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -300,6 +300,7 @@ let translate_v7_string = function | "Pow_Rabsolu" -> "Pow_Rabs" ... *) + | "complet" -> "completeness" | "Rle_sym1" -> "Rle_ge" | "Rmin_sym" -> "Rmin_comm" | "Rsqr_times" -> "Rsqr_mult" @@ -427,7 +428,8 @@ let same c d = try check_same_type c d; true with _ -> false (**********************************************************************) (* conversion of terms and cases patterns *) -let make_current_scope (scopt,scopes) = option_cons scopt scopes +let make_current_scopes (scopt,scopes) = + option_fold_right push_scope scopt scopes let rec extern_cases_pattern_in_scope scopes vars pat = try @@ -711,7 +713,7 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) = extern inctx scopes vars c) and extern_numeral loc scopes (sc,n) = - match Symbols.availability_of_numeral sc (make_current_scope scopes) with + match Symbols.availability_of_numeral sc (make_current_scopes scopes) with | None -> raise No_match | Some key -> insert_delimiters (CNumeral (loc,n)) key @@ -732,17 +734,17 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function let e = match keyrule with | NotationRule (sc,ntn) -> - let scopes' = option_cons tmp_scope scopes in + let scopes' = make_current_scopes (tmp_scope, scopes) in (match Symbols.availability_of_notation (sc,ntn) scopes' with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> - let scopes = option_cons scopt scopes in + let scopes = make_current_scopes (scopt, scopes) in let l = List.map (fun (c,(scopt,scl)) -> extern (* assuming no overloading: *) true - (scopt,scl@scopes) vars c) + (scopt,List.fold_right push_scope scl scopes) vars c) subst in insert_delimiters (CNotation (loc,ntn,l)) key) | SynDefRule kn -> |