CLEANUP: Context.{Rel,Named}.Declaration.t

  Originally, rel-context was represented as:

    Context.rel_context = Names.Name.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
                  | LocalDef of Names.Name.t * Constr.t * Constr.t

  Originally, named-context was represented as:

    Context.named_context = Names.Id.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Named.t = LocalAssum of Names.Id.t * Constr.t
                    | LocalDef of Names.Id.t * Constr.t * Constr.t

Motivation:

  (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
      function which looked like this:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      Suppose that you do not know about rel-context and named-context.
      (that is the case of people who just started to read the source code)
      Merlin would tell you that the type of the value you are destructing
      by "match" is:

        'a * 'b option * Constr.t                    (* worst-case scenario *)

      or

        Named.Name.t * Constr.t option * Constr.t    (* best-case scenario (?) *)

      To me, this is akin to wearing an opaque veil.
      It is hard to figure out the meaning of the values you are looking at.
      In particular, it is hard to discover the connection between the value
      we are destructing above and the datatypes and functions defined
      in the "kernel/context.ml" file.

      In this case, the connection is there, but it is not visible
      (between the function above and the "Context" module).

      ------------------------------------------------------------------------

      Now consider, what happens when the reader see the same function
      presented in the following form:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
      to jump to the corresponding definition and learn more.

      In this case, the connection is there, and it is directly visible
      (between the function above and the "Context" module).

  (2) Also, if we already have the concepts such as:
      - local declaration
      - local assumption
      - local definition
      and we describe these notions meticulously in the Reference Manual,
      then it is a real pity not to reinforce the connection
      of the actual code with the abstract description we published.

1 files changed, 8 insertions, 7 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index fc3f0cc75..6b2b58531 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -22,6 +22,7 @@ open Libnames
 open Globnames
 open Environ
 open Termops
+open Context.Rel.Declaration
 
 (**********************************************************************)
 (* Conventional names *)
@@ -113,7 +114,7 @@ let hdchar env c =
     | Rel n ->
 	(if n<=k then "p" (* the initial term is flexible product/function *)
 	 else
-	   try match Environ.lookup_rel (n-k) env with
+	   try match Environ.lookup_rel (n-k) env |> to_tuple with
 	     | (Name id,_,_)   -> lowercase_first_char id
 	     | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
 	   with Not_found -> "y")
@@ -142,10 +143,9 @@ let prod_name = mkProd_name
 let prod_create   env (a,b) = mkProd (named_hd env a Anonymous, a, b)
 let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous, a, b)
 
-let name_assumption env (na,c,t) =
-  match c with
-    | None      -> (named_hd env t na, None, t)
-    | Some body -> (named_hd env body na, c, t)
+let name_assumption env = function
+    | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
+    | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
 
 let name_context env hyps =
   snd
@@ -277,11 +277,12 @@ let next_name_away = next_name_away_with_default default_non_dependent_string
 let make_all_name_different env =
   let avoid = ref (ids_of_named_context (named_context env)) in
   process_rel_context
-    (fun (na,c,t) newenv ->
+    (fun decl newenv ->
+       let (na,_,t) = to_tuple decl in
        let na = named_hd newenv t na in
        let id = next_name_away na !avoid in
        avoid := id::!avoid;
-       push_rel (Name id,c,t) newenv)
+       push_rel (set_name (Name id) decl) newenv)
     env
 
 (* 5- Looks for next fresh name outside a list; avoids also to use names that