diff options
| author | msozeau | 2008-04-02 15:47:07 +0000 |
|---|---|---|
| committer | msozeau | 2008-04-02 15:47:07 +0000 |
| commit | 46cad49197abd858ef430c150e32702c01b2f205 (patch) | |
| tree | 714d2ef2858e862f9233955260ed1d47e9963404 /interp/notation.ml | |
| parent | bf9d5245c59e297d93ee759f54b40ec67db5ff93 (diff) | |
Add the ability to specify the implicit status of section variables and
whether or not to keep them regardless of the actual dependencies (in
order to implement the proper discharge behavior for type classes).
This means adding an argument to rebuild_function in libobject, giving
this information on variables after a section's constants have been
discharged (discharge_function is too early). Surface syntax for
Variable not added yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10741 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index b04f3be035..f3ecbd446f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -467,7 +467,7 @@ let discharge_arguments_scope (_,(req,r,l)) = if req = ArgsScopeNoDischarge then None else Some (req,pop_global_reference r,l) -let rebuild_arguments_scope (req,r,l) = +let rebuild_arguments_scope (_,(req,r,l)) = match req with | ArgsScopeNoDischarge -> assert false | ArgsScopeAuto -> |