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_type.ml | 31 ++++++++++++++++---------------
 1 file changed, 16 insertions(+), 15 deletions(-)

(limited to 'proofs/proof_type.ml')

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 150fb89f..1daddde9 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
+(*i $Id$ *)
 
 (*i*)
 open Environ
@@ -48,11 +48,11 @@ type proof_tree = {
 
 and rule =
   | Prim of prim_rule
-  | Nested of compound_rule * proof_tree 
+  | Nested of compound_rule * proof_tree
   | Decl_proof of bool
   | Daimon
 
-and compound_rule=  
+and compound_rule=
   | Tactic of tactic_expr * bool
   | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
 
@@ -63,47 +63,48 @@ and tactic = goal sigma -> (goal list sigma * validation)
 and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
-  (open_constr,
+  (constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
    ltac_constant,
    identifier,
-   glob_tactic_expr)
+   glob_tactic_expr,
+   tlevel)
      Tacexpr.gen_tactic_expr
 
 and atomic_tactic_expr =
-  (open_constr,
+  (constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
    ltac_constant,
    identifier,
-   glob_tactic_expr)
+   glob_tactic_expr,
+   tlevel)
      Tacexpr.gen_atomic_tactic_expr
 
 and tactic_arg =
-  (open_constr,
+  (constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
    ltac_constant,
    identifier,
-   glob_tactic_expr)
+   glob_tactic_expr,
+   tlevel)
      Tacexpr.gen_tactic_arg
 
-type hyp_location = identifier Tacexpr.raw_hyp_location
-
-type ltac_call_kind = 
+type ltac_call_kind =
   | LtacNotationCall of string
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
   | LtacVarCall of identifier * glob_tactic_expr
   | LtacConstrInterp of rawconstr *
-      ((identifier * constr) list * (identifier * identifier option) list)
+      (extended_patvar_map * (identifier * identifier option) list)
 
-type ltac_trace = (loc * ltac_call_kind) list
+type ltac_trace = (int * loc * ltac_call_kind) list
 
-exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn
+exception LtacLocated of (int * ltac_call_kind * ltac_trace * loc) * exn
 
 let abstract_tactic_box = ref (ref None)
-- 
cgit v1.2.3