From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 proofs/proof_trees.ml | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

(limited to 'proofs/proof_trees.ml')

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 99a1e506..a5bd073a 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: proof_trees.ml 10124 2007-09-17 18:40:21Z herbelin $ *)
+(* $Id$ *)
 
 open Closure
 open Util
@@ -33,10 +33,11 @@ let is_bind = function
 
 (* Functions on goals *)
 
-let mk_goal hyps cl extra = 
-  { evar_hyps = hyps; evar_concl = cl; 
+let mk_goal hyps cl extra =
+  { evar_hyps = hyps; evar_concl = cl;
     evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
-    evar_body = Evar_empty; evar_extra = extra }
+    evar_body = Evar_empty; evar_source = (dummy_loc,GoalEvar); 
+    evar_extra = extra }
 
 (* Functions on proof trees *)
 
@@ -48,9 +49,9 @@ let ref_of_proof pf =
 let rule_of_proof pf =
   let (r,_) = ref_of_proof pf in r
 
-let children_of_proof pf = 
+let children_of_proof pf =
   let (_,cl) = ref_of_proof pf in cl
-				    
+
 let goal_of_proof pf = pf.goal
 
 let subproof_of_proof pf = match pf.ref with
@@ -68,13 +69,13 @@ let is_tactic_proof pf = match pf.ref with
   | _ -> false
 
 
-let pf_lookup_name_as_renamed env ccl s =
-  Detyping.lookup_name_as_renamed env ccl s
+let pf_lookup_name_as_displayed env ccl s =
+  Detyping.lookup_name_as_displayed env ccl s
 
 let pf_lookup_index_as_renamed env ccl n =
   Detyping.lookup_index_as_renamed env ccl n
 
-(* Functions on rules (Proof mode) *) 
+(* Functions on rules (Proof mode) *)
 
 let is_dem_rule  = function
     Decl_proof _  -> true
@@ -85,9 +86,9 @@ let is_proof_instr = function
   | _ -> false
 
 let is_focussing_command = function
-    Decl_proof b -> b 
-  | Nested (Proof_instr (b,_),_) -> b 
-  | _ -> false   
+    Decl_proof b -> b
+  | Nested (Proof_instr (b,_),_) -> b
+  | _ -> false
 
 
 (*********************************************************************)
-- 
cgit v1.2.3