Imported Upstream version 8.5~beta1+dfsg

1 files changed, 20 insertions, 71 deletions

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index c56f8a24..26bb78df 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -1,104 +1,53 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 (*i*)
-open Environ
 open Evd
 open Names
-open Libnames
 open Term
-open Util
+open Context
 open Tacexpr
-(* open Decl_expr *)
 open Glob_term
-open Genarg
 open Nametab
-open Pattern
+open Misctypes
 (*i*)
 
 (* This module defines the structure of proof tree and the tactic type. So, it
    is used by Proof_tree and Refiner *)
 
+(** Types of goals, tactics, rules ... *)
+
 type goal = Goal.goal
 
 type tactic = goal sigma -> goal list sigma 
 
 type prim_rule =
-  | Intro of identifier
-  | Cut of bool * bool * identifier * types
-  | FixRule of identifier * int * (identifier * int * constr) list * int
-  | Cofix of identifier * (identifier * constr) list * int
+  | Cut of bool * bool * Id.t * types
+  | FixRule of Id.t * int * (Id.t * int * constr) list * int
+  | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
-  | Convert_concl of types * cast_kind
-  | Convert_hyp of named_declaration
-  | Thin of identifier list
-  | ThinBody of identifier list
-  | Move of bool * identifier * identifier move_location
-  | Order of identifier list
-  | Rename of identifier * identifier
-  | Change_evars
-
-type proof_tree = {
-  goal : goal;
-  ref : (rule * proof_tree list) option }
-
-and rule =
-  | Prim of prim_rule
-  | Nested of compound_rule * proof_tree
-  | Decl_proof of bool
-  | Daimon
+  | Thin of Id.t list
+  | Move of Id.t * Id.t move_location
 
-and compound_rule=
-  | Tactic of tactic_expr * bool
+(** Nowadays, the only rules we'll consider are the primitive rules *)
 
-and tactic_expr =
-  (constr,
-   constr_pattern,
-   evaluable_global_reference,
-   inductive,
-   ltac_constant,
-   identifier,
-   glob_tactic_expr,
-   tlevel)
-     Tacexpr.gen_tactic_expr
+type rule = prim_rule
 
-and atomic_tactic_expr =
-  (constr,
-   constr_pattern,
-   evaluable_global_reference,
-   inductive,
-   ltac_constant,
-   identifier,
-   glob_tactic_expr,
-   tlevel)
-     Tacexpr.gen_atomic_tactic_expr
-
-and tactic_arg =
-  (constr,
-   constr_pattern,
-   evaluable_global_reference,
-   inductive,
-   ltac_constant,
-   identifier,
-   glob_tactic_expr,
-   tlevel)
-     Tacexpr.gen_tactic_arg
+(** Ltac traces *)
 
 type ltac_call_kind =
-  | LtacNotationCall of string
+  | LtacMLCall of glob_tactic_expr
+  | LtacNotationCall of KerName.t
   | LtacNameCall of ltac_constant
-  | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
-  | LtacVarCall of identifier * glob_tactic_expr
-  | LtacConstrInterp of glob_constr *
-      (extended_patvar_map * (identifier * identifier option) list)
-
-type ltac_trace = (int * loc * ltac_call_kind) list
+  | LtacAtomCall of glob_atomic_tactic_expr
+  | LtacVarCall of Id.t * glob_tactic_expr
+  | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map
 
-exception LtacLocated of (int * ltac_call_kind * ltac_trace * loc) * exn
+type ltac_trace = (Loc.t * ltac_call_kind) list
 
-let abstract_tactic_box = ref (ref None)
+let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()