Merge branch 'master' into ltac2-hooks

10 files changed, 138 insertions, 206 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6bc2a4f94..8a49cd548 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1245,6 +1245,12 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   let typs = List.map2 RelDecl.set_name names cs_args
   in
 
+  (* Beta-iota-normalize types to better compatibility of refine with 8.4 behavior *)
+  (* This is a bit too strong I think, in the sense that what we would *)
+  (* really like is to have beta-iota reduction only at the positions where *)
+  (* parameters are substituted *)
+  let typs = List.map (map_type (nf_betaiota !(pb.evdref))) typs in
+
   (* We build the matrix obtained by expanding the matching on *)
   (* "C x1..xn as x" followed by a residual matching on eqn into *)
   (* a matching on "x1 .. xn eqn" *)
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index e18625c42..bd7350dc4 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -175,6 +175,19 @@ let cofixp_reducible flgs _ stk =
   else
     false
 
+let debug_cbv = ref false
+let _ = Goptions.declare_bool_option {
+  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optname = "cbv visited constants display";
+  Goptions.optkey = ["Debug";"Cbv"];
+  Goptions.optread = (fun () -> !debug_cbv);
+  Goptions.optwrite = (fun a -> debug_cbv:=a);
+}
+
+let pr_key = function
+  | ConstKey (sp,_) -> Names.Constant.print sp
+  | VarKey id -> Names.Id.print id
+  | RelKey n -> Pp.(str "REL_" ++ int n)
 
 (* The main recursive functions
  *
@@ -254,9 +267,17 @@ let rec norm_head info env t stack =
 and norm_head_ref k info env stack normt =
   if red_set_ref (info_flags info) normt then
     match ref_value_cache info normt with
-      | Some body -> strip_appl (shift_value k body) stack
-      | None -> (VAL(0,make_constr_ref k normt),stack)
-  else (VAL(0,make_constr_ref k normt),stack)
+      | Some body ->
+         if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt);
+         strip_appl (shift_value k body) stack
+      | None ->
+         if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt);
+         (VAL(0,make_constr_ref k normt),stack)
+  else
+    begin
+      if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt);
+      (VAL(0,make_constr_ref k normt),stack)
+    end
 
 (* cbv_stack_term performs weak reduction on constr t under the subs
  * env, with context stack, i.e. ([env]t stack).  First computes weak
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 2334be966..edcfa99c8 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -361,6 +361,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 
       |	PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst
       |	PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst
+      | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
+         Array.fold_left2 (sorec ctx env) subst args1 args2
       | _ -> raise PatternMatchingFailure
 
   in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1eec85f45..0d798b4d9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -422,7 +422,9 @@ let detype_sort sigma = function
   | Type u ->
     GType
       (if !print_universes
-       then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)]
+       then
+         let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in
+         [dl, Name.mk_name (Id.of_string_soft u)]
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -434,7 +436,8 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l)))
+  let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in
+  GType (Some (dl, Name.mk_name (Id.of_string_soft l)))
 
 let detype_instance sigma l = 
   let l = EInstance.kind sigma l in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f0d011477..4ada91eb5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -470,23 +470,13 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c =
 (* Managing pattern-unification *)
 (********************************)
 
-let map_all f l =
-  let rec map_aux f l = match l with
-  | [] -> []
-  | x :: l ->
-    match f x with
-    | None -> raise Exit
-    | Some y -> y :: map_aux f l
-  in
-  try Some (map_aux f l) with Exit -> None
-
 let expand_and_check_vars sigma aliases l =
   let map a = match get_alias_chain_of sigma aliases a with
   | None, [] -> Some a
   | None, a :: _ -> Some a
   | Some _, _ -> None
   in
-  map_all map l
+  Option.List.map map l
 
 let alias_distinct l =
   let rec check (rels, vars) = function
@@ -540,7 +530,7 @@ let is_unification_pattern_meta env evd nb m l t =
   | Rel n -> if n <= nb then Some (RelAlias n) else None
   | _ -> None
   in
-  match map_all map l with
+  match Option.List.map map l with
   | Some l ->
     begin match find_unification_pattern_args env evd l t with
     | Some _ as x when not (dependent evd (mkMeta m) t) -> x
@@ -550,10 +540,10 @@ let is_unification_pattern_meta env evd nb m l t =
     None
 
 let is_unification_pattern_evar env evd (evk,args) l t =
-  match map_all (fun c -> to_alias evd c) l with
+  match Option.List.map (fun c -> to_alias evd c) l with
   | Some l when noccur_evar env evd evk t ->
     let args = remove_instance_local_defs evd evk args in
-    let args = map_all (fun c -> to_alias evd c) args in
+    let args = Option.List.map (fun c -> to_alias evd c) args in
     begin match args with
     | None -> None
     | Some args ->
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index ebbfa195f..6509aaac3 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -214,120 +214,62 @@ let fold_glob_constr f acc = function
     f acc c
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
 
-let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
+let fold_return_type_with_binders f g v acc (na,tyopt) =
+  Option.fold_left (f (name_fold g na v)) acc tyopt
 
-let same_id na id = match na with
-| Anonymous -> false
-| Name id' -> Id.equal id id'
+let fold_glob_constr_with_binders g f v acc = function
+  | GVar _ -> acc
+  | GApp (_,c,args) -> List.fold_left (f v) (f v acc c) args
+  | GLambda (_,na,_,b,c) | GProd (_,na,_,b,c) ->
+    f (name_fold g na v) (f v acc b) c
+  | GLetIn (_,na,b,t,c) ->
+    f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c
+  | GCases (_,_,rtntypopt,tml,pl) ->
+    let fold_pattern acc (_,idl,p,c) = f (List.fold_right g idl v) acc c in
+    let fold_tomatch (v',acc) (tm,(na,onal)) =
+      (Option.fold_left (fun v'' (_,_,nal) -> List.fold_right (name_fold g) nal v'')
+                        (name_fold g na v') onal,
+       f v acc tm) in
+    let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in
+    let acc = Option.fold_left (f v') acc rtntypopt in
+    List.fold_left fold_pattern acc pl
+  | GLetTuple (_,nal,rtntyp,b,c) ->
+    f v (f v (fold_return_type_with_binders f g v acc rtntyp) b) c
+  | GIf (_,c,rtntyp,b1,b2) ->
+    f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2
+  | GRec (_,_,idl,bll,tyl,bv) ->
+    let f' i acc fid =
+      let v,acc =
+	List.fold_left
+	  (fun (v,acc) (na,k,bbd,bty) ->
+            (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty))
+          (v,acc)
+          bll.(i) in
+      f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in
+    Array.fold_left_i f' acc idl
+  | GCast (_,c,k) ->
+    let acc = match k with
+      | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
+    f v acc c
+  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
+
+let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
 let occur_glob_constr id =
-  let rec occur = function
+  let rec occur barred acc = function
     | GVar (loc,id') -> Id.equal id id'
-    | GApp (loc,f,args) -> (occur f) || (List.exists occur args)
-    | GLambda (loc,na,bk,ty,c) ->
-      (occur ty) || (not (same_id na id) && (occur c))
-    | GProd (loc,na,bk,ty,c) ->
-      (occur ty) || (not (same_id na id) && (occur c))
-    | GLetIn (loc,na,b,t,c) ->
-      (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c))
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
-	(occur_option rtntypopt)
-        || (List.exists (fun (tm,_) -> occur tm) tml)
-	|| (List.exists occur_pattern pl)
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
-	occur_return_type rtntyp id
-        || (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c))
-    | GIf (loc,c,rtntyp,b1,b2) ->
-	occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2)
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
-        not (Array.for_all4 (fun fid bl ty bd ->
-          let rec occur_fix = function
-              [] -> not (occur ty) && (Id.equal fid id || not(occur bd))
-            | (na,k,bbd,bty)::bl ->
-                not (occur bty) &&
-                (match bbd with
-                    Some bd -> not (occur bd)
-                  | _ -> true) &&
-                (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in
-          occur_fix bl)
-          idl bl tyl bv)
-    | GCast (loc,c,k) -> (occur c) || (match k with CastConv t
-      | CastVM t | CastNative t -> occur t | CastCoerce -> false)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false
-
-  and occur_pattern (loc,idl,p,c) = not (Id.List.mem id idl) && (occur c)
-
-  and occur_option = function None -> false | Some p -> occur p
-
-  and occur_return_type (na,tyopt) id = not (same_id na id) && occur_option tyopt
-
-  in occur
-
-
-let add_name_to_ids set na =
-  match na with
-    | Anonymous -> set
-    | Name id -> Id.Set.add id set
+    | c ->
+       (* [g] looks if [id] appears in a binding position, in which
+          case, we don't have to look in the corresponding subterm *)
+       let g id' barred = barred || Id.equal id id' in
+       let f barred acc c = acc || not barred && occur false acc c in
+       fold_glob_constr_with_binders g f barred acc c in
+  occur false false
 
 let free_glob_vars =
-  let rec vars bounded vs = function
-    | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
-    | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
-    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
-	let vs' = vars bounded vs ty in
-	let bounded' = add_name_to_ids bounded na in
-       vars bounded' vs' c
-    | GLetIn (loc,na,b,ty,c) ->
-	let vs' = vars bounded vs b in
-	let vs'' = Option.fold_left (vars bounded) vs' ty in
-	let bounded' = add_name_to_ids bounded na in
-       vars bounded' vs'' c
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
-	let vs1 = vars_option bounded vs rtntypopt in
-	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
-	List.fold_left (vars_pattern bounded) vs2 pl
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
-	let vs1 = vars_return_type bounded vs rtntyp in
-	let vs2 = vars bounded vs1 b in
-	let bounded' = List.fold_left add_name_to_ids bounded nal in
-	vars bounded' vs2 c
-    | GIf (loc,c,rtntyp,b1,b2) ->
-	let vs1 = vars_return_type bounded vs rtntyp in
-	let vs2 = vars bounded vs1 c in
-	let vs3 = vars bounded vs2 b1 in
-	vars bounded vs3 b2
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
-	let bounded' = Array.fold_right Id.Set.add idl bounded in
-	let vars_fix i vs fid =
-	  let vs1,bounded1 =
-	    List.fold_left
-	      (fun (vs,bounded) (na,k,bbd,bty) ->
-		 let vs' = vars_option bounded vs bbd in
-		 let vs'' = vars bounded vs' bty in
-		 let bounded' = add_name_to_ids bounded na in
-		 (vs'',bounded')
-	      )
-	      (vs,bounded')
-	      bl.(i)
-	  in
-	  let vs2 = vars bounded1 vs1 tyl.(i) in
-	  vars bounded1 vs2 bv.(i)
-	in
-	Array.fold_left_i vars_fix vs idl
-    | GCast (loc,c,k) -> let v = vars bounded vs c in
-	(match k with CastConv t | CastVM t | CastNative t -> vars bounded v t | _ -> v)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
-
-  and vars_pattern bounded vs (loc,idl,p,c) =
-    let bounded' = List.fold_right Id.Set.add idl bounded  in
-    vars bounded' vs c
-
-  and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p
-
-  and vars_return_type bounded vs (na,tyopt) =
-    let bounded' = add_name_to_ids bounded na in
-    vars_option bounded' vs tyopt
-  in
+  let rec vars bound vs = function
+    | GVar (loc,id') -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs
+    | c -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in
   fun rt ->
     let vs = vars Id.Set.empty Id.Set.empty rt in
     Id.Set.elements vs
@@ -353,57 +295,16 @@ let add_and_check_ident id set =
   Id.Set.add id set
 
 let bound_glob_vars =
-  let rec vars bound = function
-    | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c ->
-        let bound = name_fold add_and_check_ident na bound in
-        fold_glob_constr vars bound c
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
-	let bound = vars_option bound rtntypopt in
-	let bound =
-          List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in
-	List.fold_left vars_pattern bound pl
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
-	let bound = vars_return_type bound rtntyp in
-	let bound = vars bound b in
-	let bound = List.fold_right (name_fold add_and_check_ident) nal bound in
-	vars bound c
-    | GIf (loc,c,rtntyp,b1,b2) ->
-	let bound = vars_return_type bound rtntyp in
-	let bound = vars bound c in
-	let bound = vars bound b1 in
-	vars bound b2
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
-	let bound = Array.fold_right Id.Set.add idl bound in
-	let vars_fix i bound fid =
-	  let bound =
-	    List.fold_left
-	      (fun bound (na,k,bbd,bty) ->
-		 let bound = vars_option bound bbd in
-		 let bound = vars bound bty in
-		 name_fold add_and_check_ident na bound
-	      )
-	      bound
-	      bl.(i)
-	  in
-	  let bound = vars bound tyl.(i) in
-	  vars bound bv.(i)
-	in
-	Array.fold_left_i vars_fix bound idl
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound
-    | GApp _ | GCast _ as c -> fold_glob_constr vars bound c
-
-  and vars_pattern bound (loc,idl,p,c) =
-    let bound = List.fold_right add_and_check_ident idl bound in
-    vars bound c
-
-  and vars_option bound = function None -> bound | Some p -> vars bound p
-
-  and vars_return_type bound (na,tyopt) =
-    let bound = name_fold add_and_check_ident na bound in
-    vars_option bound tyopt
+  let rec vars bound =
+    fold_glob_constr_with_binders
+      (fun id () -> bound := add_and_check_ident id !bound)
+      (fun () () -> vars bound)
+      () ()
   in
   fun rt ->
-    vars Id.Set.empty rt
+    let bound = ref Id.Set.empty in
+    vars bound rt;
+    !bound
 
 (** Mapping of names in binders *)
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 55e6b6533..af2834e49 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -37,6 +37,7 @@ val map_glob_constr_left_to_right :
 val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit
 
 val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
+val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : Id.t -> glob_constr -> bool
 val free_glob_vars : glob_constr -> Id.t list
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 7fe81c9a4..1669f8334 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -30,7 +30,7 @@ let smartmap_cast_type f c =
 let glob_sort_eq g1 g2 = match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
-| GType l1, GType l2 -> List.equal (fun x y -> CString.equal (snd x) (snd y)) l1 l2
+| GType l1, GType l2 -> List.equal (fun x y -> Names.Name.equal (snd x) (snd y)) l1 l2
 | _ -> false
 
 let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 33a68589c..a22db1407 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -159,7 +159,9 @@ let pattern_of_constr env sigma t =
       (match snd (Evd.evar_source evk sigma) with
       | Evar_kinds.MatchingVar (b,id) ->
         assert (not b); PMeta (Some id)
-      | Evar_kinds.GoalEvar -> 
+      | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
+        (* These are the two evar kinds used for existing goals *)
+        (* see Proofview.mark_in_evm *)
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
       | _ -> 
 	 PMeta None)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index fa37f8cf6..7b9d9ae4b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -192,45 +192,51 @@ let _ =
 	    optwrite = (:=) Universes.set_minimization })
 						  
 (** Miscellaneous interpretation functions *)
-let interp_universe_level_name evd (loc,s) =
-  let names, _ = Global.global_universe_names () in
-    if CString.string_contains ~where:s ~what:"." then
-      match List.rev (CString.split '.' s) with
-      | [] -> anomaly (str"Invalid universe name " ++ str s)
-      | n :: dp -> 
-	 let num = int_of_string n in
-	 let dp = DirPath.make (List.map Id.of_string dp) in
-	 let level = Univ.Level.make dp num in
-	 let evd =
-	   try Evd.add_global_univ evd level
-	   with UGraph.AlreadyDeclared -> evd
-	 in evd, level
-    else 
-      try
-	let level = Evd.universe_of_name evd s in
-	evd, level
-      with Not_found ->
-	try 
-	  let id = try Id.of_string s with _ -> raise Not_found in
-          evd, snd (Idmap.find id names)
-	with Not_found -> 
-	  if not (is_strict_universe_declarations ()) then
-  	    new_univ_level_variable ~loc ~name:s univ_rigid evd
-	  else user_err ~loc ~hdr:"interp_universe_level_name"
-			     (Pp.(str "Undeclared universe: " ++ str s))
+let interp_universe_level_name ~anon_rigidity evd (loc,s) =
+  match s with
+  | Anonymous ->
+     new_univ_level_variable ~loc anon_rigidity evd
+  | Name s ->
+     let s = Id.to_string s in
+     let names, _ = Global.global_universe_names () in
+     if CString.string_contains ~where:s ~what:"." then
+       match List.rev (CString.split '.' s) with
+       | [] -> anomaly (str"Invalid universe name " ++ str s)
+       | n :: dp ->
+	  let num = int_of_string n in
+	  let dp = DirPath.make (List.map Id.of_string dp) in
+	  let level = Univ.Level.make dp num in
+	  let evd =
+	    try Evd.add_global_univ evd level
+	    with UGraph.AlreadyDeclared -> evd
+	  in evd, level
+     else
+       try
+	 let level = Evd.universe_of_name evd s in
+	 evd, level
+       with Not_found ->
+	 try
+	   let id = try Id.of_string s with _ -> raise Not_found in
+           evd, snd (Idmap.find id names)
+	 with Not_found ->
+	   if not (is_strict_universe_declarations ()) then
+  	     new_univ_level_variable ~loc ~name:s univ_rigid evd
+	   else user_err ~loc ~hdr:"interp_universe_level_name"
+		  (Pp.(str "Undeclared universe: " ++ str s))
 
 let interp_universe ?loc evd = function
   | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
 	    evd, Univ.Universe.make l
   | l ->
     List.fold_left (fun (evd, u) l -> 
-      let evd', l = interp_universe_level_name evd l in
+        (* [univ_flexible_alg] can produce algebraic universes in terms *)
+        let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in
 	(evd', Univ.sup u (Univ.Universe.make l)))
     (evd, Univ.Universe.type0m) l
 
 let interp_level_info loc evd : Misctypes.level_info -> _ = function
   | None -> new_univ_level_variable ~loc univ_rigid evd
-  | Some (loc,s) -> interp_universe_level_name evd (loc,s)
+  | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (loc,s)
 
 let interp_sort ?loc evd = function
   | GProp -> evd, Prop Null