summaryrefslogtreecommitdiff
path: root/proofs/tacexpr.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /proofs/tacexpr.ml
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'proofs/tacexpr.ml')
-rw-r--r--proofs/tacexpr.ml26
1 files changed, 10 insertions, 16 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 8e51171f..66136afa 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: tacexpr.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: tacexpr.ml 11739 2009-01-02 19:33:19Z herbelin $ i*)
open Names
open Topconstr
@@ -58,12 +58,7 @@ let make_red_flag =
add_flag
{rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
-type hyp_location_flag = (* To distinguish body and type of local defs *)
- | InHyp
- | InHypTypeOnly
- | InHypValueOnly
-
-type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag
+type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag
type 'id move_location =
| MoveAfter of 'id
@@ -103,7 +98,6 @@ type 'id message_token =
| MsgInt of int
| MsgIdent of 'id
-
type 'id gsimple_clause = ('id raw_hyp_location) option
(* onhyps:
[None] means *on every hypothesis*
@@ -133,16 +127,15 @@ type multi =
| RepeatStar
| RepeatPlus
-type pattern_expr = constr_expr
-
(* Type of patterns *)
type 'a match_pattern =
| Term of 'a
- | Subterm of identifier option * 'a
+ | Subterm of bool * identifier option * 'a
(* Type of hypotheses for a Match Context rule *)
type 'a match_context_hyps =
| Hyp of name located * 'a match_pattern
+ | Def of name located * 'a match_pattern * 'a match_pattern
(* Type of a Match rule for Match Context and Match *)
type ('a,'t) match_rule =
@@ -158,7 +151,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacExact of 'constr
| TacExactNoCheck of 'constr
| TacVmCastNoCheck of 'constr
- | TacApply of advanced_flag * evars_flag * 'constr with_bindings list
+ | TacApply of advanced_flag * evars_flag * 'constr with_bindings list *
+ ('id * intro_pattern_expr located option) option
| TacElim of evars_flag * 'constr with_bindings *
'constr with_bindings option
| TacElimType of 'constr
@@ -170,7 +164,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacCofix of identifier option
| TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list
| TacCut of 'constr
- | TacAssert of 'tac option * intro_pattern_expr located * 'constr
+ | TacAssert of 'tac option * intro_pattern_expr located option * 'constr
| TacGeneralize of ('constr with_occurrences * name) list
| TacGeneralizeDep of 'constr
| TacLetTac of name * 'constr * 'id gclause * letin_flag
@@ -287,7 +281,7 @@ and glob_tactic_expr =
type raw_tactic_expr =
(constr_expr,
- pattern_expr,
+ constr_pattern_expr,
reference or_by_notation,
reference or_by_notation,
reference,
@@ -296,7 +290,7 @@ type raw_tactic_expr =
type raw_atomic_tactic_expr =
(constr_expr, (* constr *)
- pattern_expr, (* pattern *)
+ constr_pattern_expr, (* pattern *)
reference or_by_notation, (* evaluable reference *)
reference or_by_notation, (* inductive *)
reference, (* ltac reference *)
@@ -305,7 +299,7 @@ type raw_atomic_tactic_expr =
type raw_tactic_arg =
(constr_expr,
- pattern_expr,
+ constr_pattern_expr,
reference or_by_notation,
reference or_by_notation,
reference,