diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-19 17:15:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-19 17:15:49 +0000 |
| commit | 3319ae45b302f17c76dd19ff95c9785d9ba04557 (patch) | |
| tree | c48b466a95276e75711a27051c2f709d9fd6bd14 /proofs/proof_type.ml | |
| parent | bc1168a4aa0a336e9686b57cc29ec562aa379973 (diff) | |
Made the interpretation levels rlevel/glevel/tlevel truly phantom
types so that the type of terms in Genarg can be changed w/o in full
independence of the level.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12599 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 29417e8b6..e7bca648c 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -69,7 +69,8 @@ and tactic_expr = inductive, ltac_constant, identifier, - glob_tactic_expr) + glob_tactic_expr, + tlevel) Tacexpr.gen_tactic_expr and atomic_tactic_expr = @@ -79,7 +80,8 @@ and atomic_tactic_expr = inductive, ltac_constant, identifier, - glob_tactic_expr) + glob_tactic_expr, + tlevel) Tacexpr.gen_atomic_tactic_expr and tactic_arg = @@ -89,7 +91,8 @@ and tactic_arg = inductive, ltac_constant, identifier, - glob_tactic_expr) + glob_tactic_expr, + tlevel) Tacexpr.gen_tactic_arg type ltac_call_kind = |