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 /contrib/subtac | |
| 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 'contrib/subtac')
| -rw-r--r-- | contrib/subtac/subtac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index e7a727bb5d..ac4b9642e7 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -100,7 +100,7 @@ let declare_assumption env isevars idl is_coe k bl c nl = Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None in let c = solve_tccs_in_type env id isevars evm c typ in - List.iter (Command.declare_one_assumption is_coe k c imps nl) idl + List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") |