diff options
| author | herbelin | 2005-01-02 08:47:14 +0000 |
|---|---|---|
| committer | herbelin | 2005-01-02 08:47:14 +0000 |
| commit | 2dee039338e6f130447741b67f36eba666131b8a (patch) | |
| tree | b7ac63eb7f7cc87edfa0056e7c69653fd6c802a1 /library | |
| parent | da705691fc9cf7724f78f4ed0cc8b93c4d7bc08e (diff) | |
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de printers dans ocamldebug
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/declare.ml b/library/declare.ml index ecf223ae00..2109c63254 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -105,7 +105,7 @@ let (in_variable, out_variable) = let declare_variable_common id obj = let oname = add_leaf id (in_variable (id,obj)) in declare_var_implicits id; - Symbols.declare_ref_arguments_scope (VarRef id); + Notation.declare_ref_arguments_scope (VarRef id); oname (* for initial declaration *) @@ -192,7 +192,7 @@ let declare_constant_common id discharged_hyps (cd,kind) = let (sp,kn as oname) = add_leaf id (in_constant (cd,kind)) in let kn = constant_of_kn kn in declare_constant_implicits kn; - Symbols.declare_ref_arguments_scope (ConstRef kn); + Notation.declare_ref_arguments_scope (ConstRef kn); Dischargedhypsmap.set_discharged_hyps sp discharged_hyps; kn @@ -290,9 +290,9 @@ let (in_inductive, out_inductive) = let declare_inductive_argument_scopes kn mie = list_iter_i (fun i {mind_entry_consnames=lc} -> - Symbols.declare_ref_arguments_scope (IndRef (kn,i)); + Notation.declare_ref_arguments_scope (IndRef (kn,i)); for j=1 to List.length lc do - Symbols.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); + Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j)); done) mie.mind_entry_inds let declare_inductive_common mie = |