summaryrefslogtreecommitdiff
path: root/proofs/tacexpr.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /proofs/tacexpr.ml
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'proofs/tacexpr.ml')
-rw-r--r--proofs/tacexpr.ml35
1 files changed, 13 insertions, 22 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 563d073a..b8279b8f 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -1,18 +1,16 @@
(************************************************************************)
(* 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: tacexpr.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Names
open Topconstr
open Libnames
open Nametab
-open Rawterm
+open Glob_term
open Util
open Genarg
open Pattern
@@ -29,7 +27,7 @@ type split_flag = bool (* true = exists false = split *)
type hidden_flag = bool (* true = internal use false = user-level *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
-type raw_red_flag =
+type glob_red_flag =
| FBeta
| FIota
| FZeta
@@ -107,14 +105,6 @@ type 'id gclause =
let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr}
-let goal_location_of = function
-| { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr ->
- Some scl
-| { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr ->
- None
-| _ ->
- error "Not a simple \"in\" clause (one hypothesis or the conclusion)"
-
type 'constr induction_clause =
('constr with_bindings induction_arg list * 'constr with_bindings option *
(intro_pattern_expr located option * intro_pattern_expr located option))
@@ -201,7 +191,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
| TacRight of evars_flag * 'constr bindings
| TacSplit of evars_flag * split_flag * 'constr bindings list
| TacAnyConstructor of evars_flag * 'tac option
- | TacConstructor of evars_flag * int or_metaid * 'constr bindings
+ | TacConstructor of evars_flag * int or_var * 'constr bindings
(* Conversion *)
| TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id gclause
@@ -239,6 +229,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr =
| TacTry of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
| TacOrelse of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
| TacDo of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
+ | TacTimeout of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
| TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
| TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
| TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * identifier option
@@ -249,7 +240,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr =
| TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list
| TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list
| TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast
- | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg
+ | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg located
and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast =
identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
@@ -272,8 +263,8 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg =
(* Globalized tactics *)
and glob_tactic_expr =
- (rawconstr_and_expr,
- rawconstr_and_expr * constr_pattern,
+ (glob_constr_and_expr,
+ glob_constr_and_expr * constr_pattern,
evaluable_global_reference and_short_name or_var,
inductive or_var,
ltac_constant located or_var,
@@ -317,8 +308,8 @@ type raw_red_expr =
(constr_expr, reference or_by_notation, constr_expr) red_expr_gen
type glob_atomic_tactic_expr =
- (rawconstr_and_expr,
- rawconstr_and_expr * constr_pattern,
+ (glob_constr_and_expr,
+ glob_constr_and_expr * constr_pattern,
evaluable_global_reference and_short_name or_var,
inductive or_var,
ltac_constant located or_var,
@@ -327,8 +318,8 @@ type glob_atomic_tactic_expr =
glevel) gen_atomic_tactic_expr
type glob_tactic_arg =
- (rawconstr_and_expr,
- rawconstr_and_expr * constr_pattern,
+ (glob_constr_and_expr,
+ glob_constr_and_expr * constr_pattern,
evaluable_global_reference and_short_name or_var,
inductive or_var,
ltac_constant located or_var,
@@ -339,7 +330,7 @@ type glob_tactic_arg =
type glob_generic_argument = glevel generic_argument
type glob_red_expr =
- (rawconstr_and_expr, evaluable_global_reference or_var, constr_pattern)
+ (glob_constr_and_expr, evaluable_global_reference or_var, constr_pattern)
red_expr_gen
type typed_generic_argument = tlevel generic_argument