Proof_using: new syntax + suggestion

Proof using can be followed by:
- All : all variables
- Type : all variables occurring in the type
- expr:
    - (a b .. c) : set
    - expr + expr : set union
    - expr - expr : set difference
    - -expr : set complement (All - expr)
Exceptions:
- a singleton set can be written without parentheses. This also allows
  the implementation of named sets sharing the same name space of
  section hyps ans write
  - bla - x : where bla is defined as (a b .. x y) elsewhere.
- if expr is just a set, then parentheses can be omitted

This module also implements some AI to tell the user how he could
decorate "Proof" with a "using BLA" clause.

Finally, one can Set Default Proof Using "str" to any string that is
used whenever the "using ..." part is missing.  The coding of this
sucks a little since it is the parser that applies the default.

1 files changed, 4 insertions, 0 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 80da457670..55901bce93 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -135,6 +135,9 @@ let record_aux env s1 s2 =
         (keep_hyps env (Id.Set.union s1 s2))) in
   Aux_file.record_in_aux "context_used" v
 
+let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
+let set_suggest_proof_using f = suggest_proof_using := f
+
 let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
@@ -159,6 +162,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
             ignore(Future.join cst);
             let vars =
               global_vars_set env (Lazyconstr.force_opaque (Future.join lc)) in
+            !suggest_proof_using kn env vars ids_typ context_ids;
             if !Flags.compilation_mode = Flags.BuildVo then
               record_aux env ids_typ vars;
             vars