Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 8 insertions, 14 deletions

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 46fce6ae..e256794a 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (*i*)
 open Environ
 open Evd
@@ -16,8 +14,8 @@ open Libnames
 open Term
 open Util
 open Tacexpr
-open Decl_expr
-open Rawterm
+(* open Decl_expr *)
+open Glob_term
 open Genarg
 open Nametab
 open Pattern
@@ -26,6 +24,10 @@ open Pattern
 (* This module defines the structure of proof tree and the tactic type. So, it
    is used by Proof_tree and Refiner *)
 
+type goal = Goal.goal
+
+type tactic = goal sigma -> goal list sigma 
+
 type prim_rule =
   | Intro of identifier
   | Cut of bool * bool * identifier * types
@@ -42,7 +44,6 @@ type prim_rule =
   | Change_evars
 
 type proof_tree = {
-  open_subgoals : int;
   goal : goal;
   ref : (rule * proof_tree list) option }
 
@@ -54,13 +55,6 @@ and rule =
 
 and compound_rule=
   | Tactic of tactic_expr * bool
-  | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
-
-and goal = evar_info
-
-and tactic = goal sigma -> (goal list sigma * validation)
-
-and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
   (constr,
@@ -100,7 +94,7 @@ type ltac_call_kind =
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
   | LtacVarCall of identifier * glob_tactic_expr
-  | LtacConstrInterp of rawconstr *
+  | LtacConstrInterp of glob_constr *
       (extended_patvar_map * (identifier * identifier option) list)
 
 type ltac_trace = (int * loc * ltac_call_kind) list