diff options
| author | barras | 2008-11-26 15:12:01 +0000 |
|---|---|---|
| committer | barras | 2008-11-26 15:12:01 +0000 |
| commit | 2e7eb4d3049b3d26d1efbe3843a68c63f8a21648 (patch) | |
| tree | 5ec956afe14106f14820907b0cbc454df4137485 /proofs/proof_type.ml | |
| parent | eaffc4814c22f879377cb1a6f76a18409e7e81e4 (diff) | |
closed bug 1898: fold x in x; added a reordering primitive tactic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11632 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 6f8aebf0ef..dabc84ca31 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -37,6 +37,7 @@ type prim_rule = | 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 |