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/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 69c1dfb47..4fb411202 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -20,6 +20,7 @@ open Vars
 open Pattern
 open Patternops
 open Misctypes
+open Context.Rel.Declaration
 (*i*)
 
 (* Given a term with second-order variables in it,
@@ -254,15 +255,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
           sorec ctx env subst c1 c2
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
-	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env)
+	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
-	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env)
+	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
-	  sorec ((na1,na2,t2)::ctx) (Environ.push_rel (na2,Some c2,t2) env)
+	  sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
@@ -271,7 +272,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 	  let n = Context.Rel.length ctx_b2 in
           let n' = Context.Rel.length ctx_b2' in
 	  if noccur_between 1 n b2 && noccur_between 1 n' b2' then
-            let f l (na,_,t) = (Anonymous,na,t)::l in
+            let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,t)::l in
 	    let ctx_br = List.fold_left f ctx ctx_b2 in
 	    let ctx_br' = List.fold_left f ctx ctx_b2' in
 	    let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
@@ -367,21 +368,21 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
       | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2))
       | _ -> assert false
       in
-      let env' = Environ.push_rel (x,None,c1) env in
+      let env' = Environ.push_rel (LocalAssum (x,c1)) env in
       try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | Prod (x,c1,c2) ->
       let next_mk_ctx = function
       | [c1; c2] -> mk_ctx (mkProd (x, c1, c2))
       | _ -> assert false
       in
-      let env' = Environ.push_rel (x,None,c1) env in
+      let env' = Environ.push_rel (LocalAssum (x,c1)) env in
       try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | LetIn (x,c1,t,c2) ->
       let next_mk_ctx = function
       | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2))
       | _ -> assert false
       in
-      let env' = Environ.push_rel (x,Some c1,t) env in
+      let env' = Environ.push_rel (LocalDef (x,c1,t)) env in
       try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | App (c1,lc) ->
         let topdown = true in