diff options
Diffstat (limited to 'proofs/tacexpr.ml')
| -rw-r--r-- | proofs/tacexpr.ml | 35 |
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 |